- Bashar Igried Deb Alkhawaldeh, Integration of the Process Algebra CSP in Dependent Type Theory -- Formalisation and Verification (Supervisor Anton Setzer), Swansea University, April 2018.
- Kristoffer Just Andersen: Automatic Program Verification, Aarhus University, Nov. 2019.
- Henning Basold, Mixed Inductive-Coinductive Reasoning Types, Programs and Logic, Radboud Universiteit Nijmegen, 2018.
- Pierre Boutry, On the formalization of foundations of geometry, University of Strasbourg, France, November 2018
- Simon Boulier, Extending type theory with syntactic models, University of Nantes, France, November 2018.
- Andrea Condoluci, β-conversion, efficiently, Università di Bologna, April 2020.
- Germán Andrés Delbianco, Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency (Supervisor A. Nanevski), Universidad Politécnica de Madrid, Escuela Técnica Superior de Ingenieros Informáticos, July 2017
- Boris Djalal, Coq formalisations for deciding problems in real algebraic geometry, Université Côte d'Azur, December 2018
- Florent Faissole, Formalizations of error analysis in numerical analysis and floating-point arithmetic, Paris-Saclay University, December 2019.
- Andrea Gabrielli, Defining, calculating and reasoning in Higher-Order Logic: Complex and Hypercomplex Analysis and applications (Supervisor Marco Maggesi), University of Florence, Italy, October, 2018.
- Gaëtan Gilbert,A type theory with definitional proof-irrelevance, University of Nantes, France, December 2019
- Andrej Dudenhefner, Algorithmic Aspects of Type-based Program Synthesis, (Supervisor J. Rehof), Technical University of Dortmund, 2019.
- Thibault Gauthier, Learning-Assisted Reasoning within Proof Assistants, University of Innsbruck, December 2018.
- Marianna Girlando, On the Proof Theory of Conditional Logics (De la théorie de la démonstration pour logiques conditionnelles), University of Helsinki and University of Aix-Marseille, March 2019.
- Evmorfia Iro-Bartzia, A formalization of elliptic curves for cryptography, Paris-Saclay University, France, February 2017.
- Svetlana Jakšić, Types for Access and Memory Control, University of Novi Ssad, November 2016.
- Rodolphe Lepigre, Semantics and Implementation of an Extension of ML for Proving Programs, Université Savoie Mont Blanc, July 2017
- G. Lungu. Subtyping in Signatures. PhD thesis, Royal Holloway, Univ. of London. 2018.
- Hendrik Maarand, Operational semantics of weak sequential composition, Tallinn University of Technology, 2020 (under review, not defended yet)
- Ian Malakhovsky, On the Expressive Power of Indexed Applicative and Monadic Structures. (Supervisor S. Soloviev.) University of Toulouse 3 Paul Sabatier and IRIT, October 2019.
- Étienne Miquey, Classical realizability and side effects, University Sorbonne Paris Cité, France and Universidad de la República, Montevideo, Uruguay, November 2017
- Federico Orsanigo, Bifibrational parametricity: from zero to two dimensions, University of Strathclyde, January, 2017.
- Richard Ian Orton, Cubical models of homotopy type theory - an internal approach, University of Cambridge, February 2019.
- Marco Paviotti: Denotational Semantics in Synthetic Guarded Domain Theory, IT University of Copenhagen, October 2016.
- Ivan Prokic, Formal modeling and analysis of resource usage and sharing in distributed software systems, University of Novi Sad, January 2020.
- Jakob von Raumer, Higher Inductive Types, Inductive Families, and Inductive-Inductive Types, University of Nottingham, December 2019.
- Timothy Revell, Types, categories, actions, University of Strathclyde, January 2016.
- Damien Rouhling, Formalisation Tools for Classical Analysis − A Case Study in Control Theory, Unversité Côte d'Azur, September 2019.
- Thomas Sibut-Pinote, Investigations in Computer-Aided Mathematics : Experimentation, Computation, and Certification, École polytechnique, France, December 2017
- Lau Skorstengaard: Formal Reasoning about Capability Machines, Aarhus University, Nov. 2019.
- Stephan Alexander Spahn, Axiomatizations of Compositional Inductive-Recursive Definitions, Eberhard Karls University Tübingen, October, 2018.
- Claude Stolze, Union, intersection and dependent types in an explicitely typed lambda-calculus, (thesis director L. Liquori), INRIA Sophia Antipolis - University of Nice, December 2019.
- Niccolò Veltri, A type-theoretic study of nontermination, Tallinn University of Technology, 2017.