Completed Ph.D. Dissertation Supervision

  1. Matteo Manighetti, ``Proof theory for proof exchange,'' 9 February 2023, Ecole Doctorale de l'Institut Polytechnique de Paris. His thesis is available on HAL.
  2. Ulysse Gérard, ``Computing with relations, functions, and bindings'', 18 October 2019, Ecole Doctorale de l'Institut Polytechnique de Paris. His thesis is available on HAL.
  3. Sonia Marin, ``Modal proof theory through a focused telescope,'' 30 January 2018 (University of Paris-Saclay). Her thesis is available on HAL.
  4. Roberto Blanco, ``Applications of Foundational Proof Certificates in Theorem Proving,'' 21 December 2017 (University of Paris-Saclay) His draft version of his thesis is available here and it appears also as a report on HAL.
  5. Zakaria Chihani, ``Certification of First-order proofs in classical and intuitionistic logics,'' 2 Novmeber 2015 (Ecole Polytechnique). His thesis is available here.
  6. Ivan Gazeau, ``Safe Programming in Finite Precision: Controlling Errors and Information Leaks,'' 14 October 2013 (Ecole Polytechnique). Co-supervised with Catuscia Palamidessi.
  7. Olivier Delande, ``Symmetric Dialogue Games in the Proof Theory of Linear Logic,'' 15 October 2009 (Ecole Polytechnique). His thesis is available here and here.
  8. Vivek Nigam, ``Exploiting non-canonicity in the sequent calculus,'' 18 September 2009 (Ecole Polytechnique). Thesis is available here.
  9. David Baelde, ``A linear approach to the proof-theory of least and greatest fixed points,'' 9 December 2008 (Ecole Polytechnique). Thesis is available here.
  10. Alexis Saurin, ``Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique),'' 30 September 2008 (Ecole Polytechnique). Thesis is available here. This thesis has won the Prix de thèse de l'Ecole Polytechnique for 2009 and the Prix de thèse ASTI 2009.
  11. Alwen Tiu, ``A Logical Framework for Reasoning about Logical Specifications,'' 15 March 2004 (Pennsylvania State University). Thesis is available here.
  12. Jérémie Wajs, `Reasoning about logic programs using definitions and induction'', 10 May 2002 (Pennsylvania State University).
  13. Elaine Pimentel, ``Linear logic as a framework for specifying sequent calculus'' December 2001 (Department of Computer Science, Universidade Federal de Minas Gerais, Brazil). Co-advised with Carlos Camarão de Figueiredo.
  14. Raymond McDowell, ``Reasoning in a Logic with Definitions and Induction,'' September 1997. A description of his PhD thesis is available. (University of Pennsylvania)
  15. Chuck Liang, ``Object-language substitution and unification in meta-logic,'' September 1995. (University of Pennsylvania) (pdf)
  16. Jawahar Lal Chirimar, ``Proof Theoretic Approach To Specification Languages,'' February 1995. His thesis is available in PDF and PS formats. See also here. (University of Pennsylvania)
  17. Joshua Hodas, ``Logic Programming in Intuitionistic Linear Logic: Theory, Design, and Implementation,'' August 1993. His thesis is avaiable in PDF format. (University of Pennsylvania)
  18. John Hannan, ``Proof-theoretic methods for analysis of functional programs,'' August 1990. (University of Pennsylvania) UPenn Tech Report,
  19. Amy Felty, ``Implementing theorem provers in a higher-order logic programming language,'' August 1989. (University of Pennsylvania)
  20. Gopalan Nadathur, ``A higher-order logic as the basis for logic programming,'' December 1986. (University of Pennsylvania) (pdf)

Completed Master's Thesis Supervision

  1. Jérémie Wajs, ``Design and implementation of a theorem prover for operational semantics'', May 2000. (Pennsylvania State University).
  2. Alexander Betis, ``Object Programming, Linear Logic and Java'', December 1999. A description of his Masters thesis is available. (Pennsylvania State University).
  3. Joshua Hodas, ``Object-Oriented Programming in Logic Programming,'' May 1990. (University of Pennsylvania)
  4. Amy Felty, ``Using extended tactics to do proof transformations,'' December 1986. (University of Pennsylvania)
  5. Greg Hager, ``Computational aspects of proofs in modal logic,'' December 1985. (University of Pennsylvania)

Completed Internship Supervision

  1. Ulysse Gérard. Proof-theory for term representation, August 2015.
  2. Jean Pichon.Why moving focusing to arithmetic is more difficult than expected, ENS Cachan, 2013.
  3. Florence Clerc.Study of Double-Negation Translations and Focused Systems, Ecole Centrale Paris, 2012.
  4. Ivan Gazeau. Utilisation de lemmes en déduction modulo, LIX and ENS, 2008.
  5. Alexandre Viel. Recherche de preuve efficace dans une logique à points fixes, LIX and ENS, 2008.
  6. David Baelde. Logique linéaire et algèbre de processus. LIX and ENS, 2005. Document deals with various possible connections between proof search in logic and asynchronous computing (for example, between linear logic and the join calculus).
  7. Axelle Ziegler. Un format pour que la bisimulation soit une congruence dans les langages de processus avec mobilité. LIX and ENS, 2004. Co-supervised with Palamidessi.
  8. Emmanuel Jeandel. Logique et jugement génériques Penn State and ENS, 2001.