• Print

Completed PhD Theses

Former students of the Functional Programming Lab have completed the following PhD theses:

• Filippo Sestini: Bootstrapping Extensionality (July 2023)
• Gun Pinyo: Twisted Cubes and their Applications in Type Theory (October 2022)
• Guerric Chupin: Efficient Implementation of Expressive Modelling Language (April 2022)
• Martin Handley: Efficiency Three Ways: Tested, Verified, and Formalised (June 2020)
• Jakob von Raumer: Higher Inductive Types, Inductive Families, and Inductive-Inductive Types (Nov 2019)
• Jonathan Fowler:  Narrowing in on property-based testing (April 2019)
• Jan Bracker: Unified notions of generalised monads and applicative functors (Dec 2018)
• Ivan Perez Dominguez: Extensible and robust functional reactive programming (July 2018)
• Gabe Dijkstra: Quotient Inductive-Inductive Definitions (February 2017)
• Paolo Capriotti: Models of Type Theory with Strict Equality (November 2016)
• Ambrus Kaposi: Type theory in a type theory with quotient inductive types (November 2016)
• Jennifer Hackett: The worker/wrapper transformation: getting it right and making it better (October 2016)
• Laurence Day: The modular compilation of effects (PDF) (October 2015)
• Florent Balestrieri: The productivity of polymorphic stream equations and the composition of circular traversals (June 2015)
• Nicolai Kraus: Truncation levels in homotopy type theory (April 2015)
• Christian Sattler: On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes (March 2015)
• Li Nuo: Quotient types in type theory (January 2015)
• John Capper: Semantic methods of functional hybrid modelling (July 2014)
• Liyang Hu: Compiling concurrency correctly: verifying software transactional memory (June 2012)
• George Giorgidze: First-class models: On a noncausal language for higher-order and structurally dynamic modelling and simulation (April 2012)
• Neil Sculthorpe: Towards safe and efficient functional reactive programming (July 2011)  Code Archive
• Rawle Prince: Aspects of the theory of containers within automated theorem proving (September 2010)
• Alexander S. Green: Towards a formally verified functional quantum programming language (July 2010)
• Ondrej Rypacek: Distributive laws in programming structures (October 2009)
• Mauro Jaskelioff: Lifting of operations in modular monadic semantics (September 2009)
• James Chapman: Type checking and normalisation (January 2009)
• Wouter Swierstra: A functional specification of effects (December 2008)
• Catherine Hope: A functional semantics for space and time (PDF) (August 2008)
• Peter Morris: Constructing universes for generic programming (September 2007)
• Pablo Nogueira: Polytypic functional programming and data abstraction (PDF) (June 2006)
• Joel Wright: Compiling and reasoning about exceptions and interrupts (PDF) (Nov 2005)
• Paul Blampied: Structured recursion for non-uniform data-types (PDF) (Mar 2000)
• Anthony Daniels: A semantics for functions and behaviours (PDF) (Dec 1999)
• Colin Taylor: Formalising and reasoning about fudgets (PDF) (Dec 1998)
• Benedict Gaster: Records, variants and qualified types (PDF) (Jul 1998)