print · login   

PhD theses

  • 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, June 2020
  • 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.