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

Programming Languages at Computer Science St Andrews

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.…

    read more

  • 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…

    read more

  • 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…

    read more

  • 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…

    read more

  • 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…

    read more