Programming Languages
What we do
Programming languages enable humans to tell a computer what to do. Our research makes programming languages as easy to use as possible. Making software safer, more secure and more performant.
Theme Lead
Edwin Brady
Application Areas
- General software development
- High performance computing
- Embedded systems
- Safety critical systems
- Healthcare
- Manufacturing
- Computer vision
- Satellites
- Flying Drones
- Cyber Security
Research Topic
- Parallel and concurrent programming
- Energy efficient and green computing
- Refactoring tools and techniques
- Functional programming
- Dependent types
- Semantics of programming languages
- Formal software verification
- Programming language implementation
- Improving security of software
- Memory consistency
- Non-functional property analysis
Our Featured Projects this Year
-
Idris: Programming as a Conversation
Idris is a programming language which encourages “type-driven development”. We believe that to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. A type represents a formally defined “plan” for a program, which, in type-driven development, is then refined step by step into a complete, working program.…
-
A Proof Checker for Linear Logic
Linear logic is a refinement of traditional (or classical) logic which is conscious of resource usage, and tracks resources carefully. This logic has many applications in Computer Science (such as in the design of programming languages and resource verification tools), as well as in Quantum Information Theory and in Linguistics. This tool checks proofs in…
-
Making it easier to write correct programs
Dependently-typed programming languages, such as Idris and Agda, permit the use of logical properties to constrain the values an expression could take. This allows us to incorporate the proof that a program satisfies certain specifications directly in the program itself, making correctness guarantees an intrinsic part of an implementation. Despite this advantage, developing dependently-typed programs…
-
Efficient Representation of Functional Programs
Functional programming is a programming paradigm which comprises equations between functions operating on “abstract data”. It is a very neat and concise style that focuses on the core logic rather than catering to the details of how a computer works. However, these programs are often very inefficient to execute because of the disregard for such…
-
Java Jotters: Literate Programming in Java
This project is focused on creating a literate programming tool for the Java programming language. Literate programming can be described as the combination of documentation alongside executable code. Which enables developers to gain a greater understanding of the code they are writing, to improve developer experience, and to facilitate maintainability and readability. The code entered…