Completed Ph.D. Dissertation Supervision
- Ulysse Gérard, ``Computing with relations, functions, and
bindings'', 18 October 2019, Ecole Doctorale de l'Institut
Polytechnique de Paris. His thesis is available
Sonia Marin, ``Modal proof theory through a focused telescope,'' 30
January 2018 (University of Paris-Saclay). Her thesis is available
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.
Zakaria Chihani, ``Certification of First-order proofs in classical
and intuitionistic logics,'' 2 Novmeber 2015 (Ecole Polytechnique).
His thesis is available here.
Ivan Gazeau, ``Safe Programming in Finite Precision: Controlling
Errors and Information Leaks,'' 14 October 2013 (Ecole
Polytechnique). Co-supervised with Catuscia Palamidessi.
Delande, ``Symmetric Dialogue Games in the Proof Theory of
Linear Logic,'' 15 October 2009 (Ecole Polytechnique). His thesis is
``Exploiting non-canonicity in the sequent calculus,'' 18 September
2009 (Ecole Polytechnique). Thesis
is available here.
David Baelde, ``A linear approach to the proof-theory of least and
greatest fixed points,'' 9 December 2008 (Ecole Polytechnique). Thesis
is available here.
Alexis Saurin, ``Une étude logique du contrôle
(appliquée à la programmation fonctionnelle et
logique),'' 30 September 2008 (Ecole Polytechnique). Thesis is
This thesis has won the Prix
de thèse de l'Ecole Polytechnique for 2009 and the
de thèse ASTI 2009.
- Alwen Tiu, ``A Logical Framework for Reasoning about Logical
Specifications,'' 15 March 2004 (Pennsylvania State University).
Thesis is available here.
- Jérémie Wajs, `Reasoning about logic programs using
definitions and induction'', 10 May 2002 (Pennsylvania State University).
- 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.
- Raymond McDowell, ``Reasoning in a Logic with Definitions and
Induction,'' September 1997.
A description of his
PhD thesis is available. (University of Pennsylvania)
- Chuck Liang, ``Object-language substitution and unification in
meta-logic,'' September 1995. (University of Pennsylvania)
- Jawahar Lal Chirimar, ``Proof Theoretic Approach To Specification
Languages,'' February 1995. His thesis is available in PS format.
See also here.
(University of Pennsylvania)
- Joshua Hodas, ``Logic Programming in Intuitionistic Linear
Logic: Theory, Design, and Implementation,'' August 1993. His thesis
is avaiable in PDF format.
(University of Pennsylvania)
- John Hannan, ``Proof-theoretic methods for analysis of
functional programs,'' August 1990. (University of Pennsylvania)
- Amy Felty, ``Implementing theorem provers in a higher-order logic
programming language,'' August 1989. (University of Pennsylvania)
- Gopalan Nadathur, ``A higher-order logic as the basis for logic
programming,'' December 1986. (University of Pennsylvania)
Completed Master's Thesis Supervision
- Jérémie Wajs, ``Design and implementation of a
theorem prover for operational semantics'', May 2000. (Pennsylvania
- Alexander Betis, ``Object Programming, Linear Logic and Java'',
December 1999. A description of his
Masters thesis is available. (Pennsylvania State University).
- Joshua Hodas, ``Object-Oriented Programming in Logic Programming,''
May 1990. (University of Pennsylvania)
- Amy Felty, ``Using extended tactics to do proof transformations,''
December 1986. (University of Pennsylvania)
- Greg Hager, ``Computational aspects of proofs in modal logic,''
December 1985. (University of Pennsylvania)
Completed Internship Supervision
- Ulysse Gérard. Proof-theory for term
representation, August 2015.
- Jean Pichon.Why moving focusing to arithmetic is more
difficult than expected, ENS Cachan, 2013.
- Florence Clerc.Study of Double-Negation Translations and
Focused Systems, Ecole Centrale Paris, 2012.
- Ivan Gazeau. Utilisation de lemmes en déduction
modulo, LIX and ENS, 2008.
- Alexandre Viel. Recherche
de preuve efficace dans une logique à points fixes,
LIX and ENS, 2008.
- 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).
- 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.
- Emmanuel Jeandel.
Logique et jugement génériques Penn State and ENS, 2001.