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