Programming Languages and Foundations

Functional programming, types, semantics, program verification, and new programming models

Programming Languages and Foundations is one of the largest research activities in LFCS. A diverse group of academic staff,  postdoctoral researchers, and PhD students are working on functional programming, types, verification, semantics, and new programming models. Our research is inspired by the vision of Robin Milner, one of the founders of LFCS, who argued "that the design of computing systems can only properly succeed if it is well grounded in theory, and that the important concepts in a theory can only emerge through protracted exposure to application."

Edinburgh LFCS is internationally recognised for major contributions to programming languages. Past contributions originating at Edinburgh include logic programming, pattern matching, parametric polymorphism, the ML programming language (leading to Standard ML, OCaml, and F#, and influencing many other languages), the use of monads for functional programming (influencing Haskell) and the use of dependent types for programming and verification.  Today, LFCS research on programming languages spans foundations and application areas ranging from databases and web programming to security and quantum computation, using techniques from category theory, type theory, operational and denotational semantics, logic, and automata theory.

Research Topics

The following topics are representative of current interests and research activity here:

Types and functional programming  Web programming, concurrency and session types; probabilistic programming and machine learning
Data-centric programming Database programming languages and language-integrated query; query and update language design; semistructured data; data provenance
Program verification and theorem proving Type theory and dependent types; algebraic specification; proof development environments (ProofGeneral); mechanized metatheory
Semantics and logics of programs Algebraic effects and effect handlers; higher-type computability; category theory, domain theory, denotational semantics
New models of computation Quantum computation;  and systems biology and concurrency

If you're interested in learning more about PL research in Edinburgh, please join the Programming Languages Interest Group mailing list, or come to one of our meetings.

Programming Languages Interest Group Mailing List


Academic staff, research staff and students affiliated with Programming Languages and Foundations

Current Projects and Related Activities

Active and recent research projects and connections to other research groups in Edinburgh and Scotland

Join Us

Opportunities to join or visit us


History of Research on Programming Languages at Edinburgh University