Completed Ph.D. Dissertation Supervision

Roberto Blanco, ``Applications of Foundational Proof Certificates
in Theorem Proving,'' 21 December 2017 (Ecole Polytechnique).
His draft version of his thesis is
available here and it appears also
as a report on HAL.

Zakaria Chihani, ``Certification of Firstorder 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). Cosupervised with Catuscia Palamidessi.

Olivier
Delande, ``Symmetric Dialogue Games in the Proof Theory of
Linear Logic,'' 15 October 2009 (Ecole Polytechnique). His thesis is
available here
and here.

Vivek Nigam,
``Exploiting noncanonicity in the sequent calculus,'' 18 September
2009 (Ecole Polytechnique). Thesis
is available here.

David Baelde, ``A linear approach to the prooftheory 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
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.
 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). Coadvised 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, ``Objectlanguage substitution and unification in
metalogic,'' September 1995. (University of Pennsylvania)
(pdf)
 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, ``Prooftheoretic methods for analysis of
functional programs,'' August 1990. (University of Pennsylvania)
 Amy Felty, ``Implementing theorem provers in a higherorder logic
programming language,'' August 1989. (University of Pennsylvania)
 Gopalan Nadathur, ``A higherorder logic as the basis for logic
programming,'' December 1986. (University of Pennsylvania)
(ps)
Completed Master's Thesis Supervision
 Jérémie Wajs, ``Design and implementation of a
theorem prover for operational semantics'', May 2000. (Pennsylvania
State University).
 Alexander Betis, ``Object Programming, Linear Logic and Java'',
December 1999. A description of his
Masters thesis is available. (Pennsylvania State University).
 Joshua Hodas, ``ObjectOriented 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.Prooftheory for term
representation, August 2015.
 Jean Pichon.Why moving focusing to arithmetic is more
difficult than expected, ENS Cachan, 2013.
 Florence Clerc.Study of DoubleNegation 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.
Cosupervised with Palamidessi.
 Emmanuel Jeandel.
Logique et jugement génériques Penn State and ENS, 2001.