Towards normalization by evaluation for the betaeta-calculus of constructions, FLOPS, pp.224-239, 2010. ,
Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991. ,
DOI : 10.1016/0304-3975(86)90035-6
Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements, 22nd IEEE Symposium on Logic in Computer Science, pp.10-12, 2007. ,
Engineering formal metatheory, POPL, pp.3-15, 2008. ,
Pure type systems with judgemental equality, Journal of Functional Programming, vol.16, issue.02, pp.219-246, 2006. ,
DOI : 10.1017/S0956796805005770
Constructions, Inductive Types and Strong Normalization, 1993. ,
Coq contribution: A formalisation of Pure Type Systems ,
Coq in Sets The Lambda Calculus: its Syntax and Semantics, Sets in Coq of Studies in Logic and the Foundations of Mathematics, 1984. ,
Lambda calculi with types, Handbook of Logic in Computer Science, pp.117-309, 1992. ,
Type Dependence and Constructive mathematics, 1988. ,
Coq in coq, 1997. ,
The duality of computation, ICFP, pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02 ,
DOI : 10.2307/2371199
Conception d'un langage de haut niveau de representation de preuves: Récurrence par filtrage de motifs; Unification en prsence de types inductifs primitifs; Synthèse de lemmes d'inversion, 1997. ,
A Linear Spine Calculus, Journal of Logic and Computation, vol.13, issue.5, pp.639-688381, 1972. ,
DOI : 10.1093/logcom/13.5.639
Expansion postponement in pure type systems ,
Hybrid: a package for higher-order syntax in isabelle and coq ,
Le langage Caml ,
Logics and Type Systems, 1993. ,
Une extension de l'interprétation fonctionelle de Gödel l'analyse et son applicationàapplication`applicationà l'´ elimination des coupures dans l'analyse et la théorie des types, Proceedings of the Second Scandinavian Logic Symposium, pp.63-92, 1971. ,
Interprétation fonctionelle etéliminationetélimination des coupures dans l'arithmétique d'ordre supérieur, 1972. ,
The undecidability of the second-order unification problem, Theor. Comput. Sci, vol.13, pp.225-230, 1981. ,
A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene, LOPSTR, pp.17-31, 2002. ,
DOI : 10.1007/3-540-45013-0_2
Cut Elimination in a Class of Sequent Calculi for Pure Type Systems, Electronic Notes in Theoretical Computer Science, vol.84, 2003. ,
DOI : 10.1016/S1571-0661(04)80848-X
On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.320-329, 1994. ,
DOI : 10.1109/LICS.1994.316057
A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure, CSL, pp.61-75, 1994. ,
URL : https://hal.archives-ouvertes.fr/inria-00381525
Séquents qu'on calcule, 1995. ,
The formulae-as-types notion of construction, pp.479-490, 1980. ,
A New Foundation for Nominal Isabelle, ITP, pp.35-50, 2010. ,
DOI : 10.1007/978-3-642-14052-5_5
Unification in Typed Lambda Calculus, Lambda-Calculus and Computer Science Theory, pp.192-212, 1975. ,
Constructive computation theory Course notes on lambda calculus, University of Bordeaux I, 2002. ,
Normalisation & Equivalence in Proof Theory & Type Theory, 2006. ,
URL : https://hal.archives-ouvertes.fr/tel-00134646
ECC: An extended calculus of constructions, Proceedings of the Fourth Annual Symposium on Logic in computer science, pp.385-395, 1989. ,
Le calcul des constructions implicite: syntaxe et sémantique, 2001. ,
A Theory of Types, 1971. ,
Intuitionistic Type Theory, Bibliopolis, 1984. ,
Pure type systems formalized, TLCA, pp.289-305, 1993. ,
DOI : 10.1007/BFb0037113
Some Lambda Calculus and Type Theory Formalized, BRICS Report Series, vol.4, issue.51, pp.373-409, 1999. ,
DOI : 10.7146/brics.v4i51.19272
A generic normalization proof for pure type systems, TYPES'96, 1997. ,
Isabelle Proof Assistant ,
Unification and anti-unification in the calculus of constructions, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.74-85, 1991. ,
DOI : 10.1109/LICS.1991.151632
Typechecking in Pure Type Systems, Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp.271-288, 1992. ,
The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions, 1994. ,
The twelf project. twelf.plparty.org ,
Formalization of equivalence between PTS and PTSe ,
Formalization of sequent calculus pure type system ,
The Celf language ,
Semantics of type theory: correctness, completeness , and independence results, 1991. ,
DOI : 10.1007/978-1-4612-0433-6
Parallel Reductions in ??-Calculus, Information and Computation, vol.118, issue.1, pp.120-127, 1995. ,
DOI : 10.1006/inco.1995.1057
Typing in pure type systems, Inf. Comput, vol.105, issue.1, pp.30-41, 1993. ,
Checking algorithms for Pure Type Systems, TYPES, pp.19-61, 1993. ,
DOI : 10.1007/3-540-58085-9_71
Une Théorie des Constructions Inductives, 1994. ,
A simple model of calculus of inductive constructions with judgemental equality ,