Personal tools
You are here: Home Research Groups and Projects Programming Languages and Foundations

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.



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

 

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.

    People

    Academic staff

     



    Myrto Arapinis

    David Aspinall

    David Aspinall

    Peter Buneman

    Peter Buneman


    AGordonParis
    
    Andrew D. Gordon
    Chris Heunen

    Chris Heunen


    John Longley
    Elham Kashefi

    Elham Kashefi



    Gordon Plotkin

    Gordon Plotkin
    Ajitha Rajan


    DonS


    Ian Stark

    Ian Stark

    Perdita Stevens

    Perdita Stevens
     



    Colin Stirling


    A photo of Philip Wadler

    Philip Wadler 

     

    Research staff

     

     

    PhD students

    Recent alumni

    Current projects

     

    Related activities

     

    There is a great deal of research activity related to programming languages in LFCS, elsewhere at Edinburgh University, and in Scotland.

     

    PhD or postdoctoral opportunities

    Possible PhD topics:

    Funded PhD studentships:

     

    More information about applying to study at LFCS


    Postdoctoral opportunities:

    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:

     

    History of Research on Programming Languages at LFCS

     

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

    Document Actions