Programming Languages and Foundations at Edinburgh
Programming Languages and Foundations is one of the largest research activities in LFCS, including 15 academic staff, 9 postdoctoral researchers, and 15 current PhD students, working on functional programming, types, verification, semantics, software engineering, language-based security and new programming models.
|| Related Activities
|| Join Us
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.
Although it is difficult to draw a sharp boundary around programming languages research at LFCS, 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); nominal logic and mechanized metatheory
- Semantics and logics of programs: algebraic effects and effect handlers; higher-type computability; category theory, domain theory, denotational semantics
- Software engineering foundations: bidirectional model transformations; quality metrics for software; software testing
- Language-based security and information assurance: types and resource-bound certification; protocol analysis and verification; privacy and anonymity
- New models of computation: quantum computation; self-explaining computation, provenance, and program slicing; 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.
Andrew D. Gordon
- Brian Campbell
- Wei Chen
- Vashti Galpin
- Sam Lindley
- James McKinna
- Garrett Morris
- Roly Perera
- Wilmer Ricciotti
- Jan Stolarek
- Danel Ahman
- Sheung Chi (Arthur) Chan
- Stefan Fehrenbach
- Simon Fowler
- Daniel Franzen
- Weili Fu
- Joseph Hallett
- Rudi Horn
- Martti Karvonen
- Pau Enrique Moliner
- Pepijn Kokke
- Craig McLaughlin
- Shayan Najd Javadipour
- Benedict Kavanagh
- Jack Williams
- Ohad Kammar (PhD -> Cambridge)
- Christopher Banks (PhD -> Roslin Institute)
- Ilias Garnier (Postdoc -> ENS Paris)
- Nassim Seghir (Postdoc -> UCL)
- From Data Types to Session Types---A Basis for Concurrency and Distribution (EPSRC)
- Nominal logic programming (Royal Society)
- A theory of least change for bidirectional transformations (EPSRC)
- REMS: Rigorous Engineering for Mainstream Systems (EPSRC)
- Language-based foundations for provenance security (AFOSR)
- Skye: A programming language bridging theory and practice for scientific data curation (ERC)
There is a great deal of research activity related to programming languages in LFCS, elsewhere at Edinburgh University, and in Scotland.
- Mobility and Security Group
- Security and Privacy Group
- Links Group
- Database Group
- Performance Evaluation Process Algebra (PEPA) Group
- Compilers and Architecture Design (CARD) Group
- Structured Parallelism Group
- Mathematical Reasoning Group (DReaM)
- Mathematically Structured Programming Group (Strathclyde)
- QUISCO: Quantum Information Scotland
- Scottish Programming Languages Seminar
Possible PhD topics:
Databases and Programming Languages: Together again for the first time (Wadler)
- Formal Verification Methods for Quantum Systems (Kashefi, Mayr)
- Integrating statically and dynamically typed languages (Wadler)
- Nominal logic, automated reasoning and type theory (Cheney)
- Proof engineering (Aspinall)
Funded PhD studentships:
- Centre for Doctoral Training in Pervasive Parallelism (10 studentships / year, 4 year MSc + PhD)
- Centre for Doctoral Training in Data Science (10 studentships / year, 4 year MSc + PhD)
- A Basis for Concurrency and Distribution (contact: Phil Wadler)
- Complexity Metrics for Testing Concurrent programs (contact: Ajitha Rajan)
- Programming languages for provenance and curation (contact: James Cheney)
- Coverage metrics for security testing (contact: Ajitha Rajan)
- Several studentships are available in Security and Privacy
Postdoctoral opportunities in programming languages at LFCS may be posted here, as available.All opportunities are officially advertised on the University jobs website.
We also welcome expressions of interest from graduating PhD students, postdoctoral researchers, or senior researchers who are considering applying for fellowships to be hosted at LFCS, including the following sources:
Programming languages and foundations have been areas of strength in Edinburgh since the 1960s. Burstall's early work on languages such as POP, NPL and Hope led to the development of pattern matching facilities now standard in most functional programming languages. Milner developed the Logic for Computable Functions (LCF), the Calculus for Communicating Systems (CCS), and the ML programming language, including an approach to polymorphic type inference that has influenced most subsequent statically-typed programming languages, including Haskell, Scala and Java. Plotkin made fundamental contributions to the semantics of programming languages, including relating call-by-name and call-by-value via continuation passing translations, exploring the semantics of concurrent and reactive systems (with Winskel), and introducing Structured Operational Semantics.
The Laboratory for Foundations of Computer Science was founded by Burstall, Milner and Plotkin in 1986. Exploring the foundations of programming through a combination of theoretical rigour and practical experimentation was an explicit goal of LFCS. Over the next quarter-century, many widely-recognised advances have been made at LFCS, including work on the Definition of Standard ML, the pi-calculus, the use of monads in semantics and functional programming, formalised mathematics, logical frameworks, dependent types, and type theory. The papers "A framework for defining logics" (Harper, Honsell, Plotkin, LICS 1987) and "Computational lambda-calculus and monads" (Moggi, LICS 1989) were recognised by LICS Test-of-Time Awards in 2007 and 2009 respectively. The paper "Imperative Functional Programming", by Peyton Jones and Wadler, won the Most Influential Paper award for POPL 1993 (awarded in 2003), and the paper "Naturally Embedded Query Languages", by Tannen, Buneman and Wong (published in ICDT 1994) won the ICDT Test of Time award in 2014. Both papers are based on Moggi's work on monads.
LFCS has grown from its original emphasis on programming languages and computational logic to cover a wide range of topics, including algorithms and complexity, databases, quantum computation, and security. Nevertheless, programming languages remains a central focus for LFCS research, and today, LFCS remains among the best environments in the world to pursue experimental and theoretical research on programming languages and computational logic. Recent students have received several best paper or best student paper awards (Willem Heijltes, LICS 2011; Antony Widjaja To, LICS 2010; Matteo Mio, ETAPS 2011). Matteo Mio also received the Ackermann Award from the European Association for Computer Science Logic in 2013, and a Kurt Gödel Research Prize Fellowship in 2014. Roope Kaivola (LFCS PhD, 1997) received the 2013 Microsoft Research Verified Software Milestone Award for work on verification of Intel's Core i7 CPU. Shayan Najd received a Google European Doctoral Fellowship in 2014.
Robin Milner was honoured with the Turing Award in 1991 for his work on LCF, CCS and ML. Milner, Burstall and Plotkin have each been honoured with the ACM SIGPLAN Programming Languages Acheivement Award, in 2001, 2009 and 2010 respectively. Plotkin was honoured with the Blaise Pascal Medal in Computer and Information Sciences from the European Academy of Sciences in 2011.
In 2012, ACM SIGPLAN established the Robin Milner Young Researcher Award to recognize outstanding contributions by young investigators in the area of programming languages. Also in 2012, the Royal Society established the Royal Society Milner Award, to recognise outstanding achievement in computer science by a European researcher. The first recipient of the Royal Society Milner Award was Gordon Plotkin, in recognition of "... his fundamental research into programming semantics with lasting impact on both the principles and design of programming languages."