Translating HOL to Dedukti, Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.74-88, 2015. ,
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412
Mixing HOL and Coq in Dedukti (Extended Abstract), Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.89-96, 2015. ,
DOI : 10.4204/EPTCS.186.9
Pure type systems with judgemental equality, Journal of Functional Programming, vol.16, issue.02, pp.219-24610, 2006. ,
DOI : 10.1017/S0956796805005770
Introducing HOL Zero, Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama Mathematical Software ? ICMS 2010, pp.142-143, 2010. ,
DOI : 10.1007/978-3-642-15582-6_25
The Common HOL Platform, Electronic Proceedings in Theoretical Computer Science, pp.42-56, 2015. ,
DOI : 10.4204/EPTCS.186.6
An introduction to mathematical logic and type theory: to truth through proof, 1986. ,
Foundational proof-carrying code, 16th Annual IEEE Symposium on Logic in Computer Science, 2001. Proceedings, pp.247-256, 2001. ,
DOI : 10.1109/lics.2001.932501
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.2076
A compact kernel for the calculus of inductive constructions, Sadhana, vol.174, issue.4, pp.71-144, 2009. ,
DOI : 10.1007/s12046-009-0003-3
The Matita Interactive Theorem Prover, Lecture Notes in Computer Science, vol.23, issue.10, pp.64-6910, 2011. ,
DOI : 10.1007/3-540-48256-3_12
Some mathematical Case Studies in ProofPower-HOL ,
A calculus of constructions with explicit subtyping, Postproceedings of the 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.27-46, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01097401
Conservativity of embeddings in the lambda-Pi calculus modulo rewriting, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs), pp.31-44, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01084165
Lambda calculi with types ,
DOI : 10.1017/cbo9781139032636
Auto-validation d'un système de preuves avec familles inductives, 1999. ,
CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo, Proof Exchange for Theorem Proving?Second International Workshop, p.44, 2012. ,
Proof by reflection In Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science An EATCS Series, pp.433-448, 2004. ,
The lambda-Pi-calculus modulo as a universal proof language, Proof Exchange for Theorem Proving -Second International Workshop, pp.28-43, 2012. ,
Foundations of constructive mathematics, 1985. ,
DOI : 10.1007/978-3-642-68952-9
Type dependence and constructive mathematics, 1989. ,
On the Role of Type Decorations in the Calculus of Inductive Constructions, Computer Science Logic, number 3634 in Lecture Notes in Computer Science, pp.151-166 ,
DOI : 10.1007/11538363_12
Inductive Types in the Calculus of Algebraic Constructions, Typed Lambda Calculi and Applications, pp.46-5910, 2003. ,
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105655
Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-9210, 2005. ,
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105648
A shallow embedding of resolution and superposition proofs into the lambda-Pi-Calculus Modulo, Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving (PxTP), pp.43-57, 2013. ,
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, pp.102-117, 2007. ,
DOI : 10.1007/978-3-540-73228-0_9
Objects and subtyping in the lambda-Pi-calculus modulo, Postproceedings of the 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics, pp.47-71, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01126394
A new type assignment for lambda-terms. Archiv für mathematische Logik und Grundlagenforschung, pp.139-156, 1978. ,
The gentle art of levitation, Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pp.3-14, 2010. ,
The calculus of constructions Information and Computation, pp.2-395, 1988. ,
Checking Zenon Modulo Proofs in Dedukti, Proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving of Electronic Proceedings in Theoretical Computer Science, pp.57-73, 2015. ,
DOI : 10.4204/EPTCS.186.7
URL : https://hal.archives-ouvertes.fr/hal-01171360
Proof certificates for first-order classical and intuitionistic logics ,
Project Abstract: Logic Atlas and Integrator (LATIN), Intelligent Computer Mathematics, number 6824 in Lecture Notes in Computer Science, pp.289-291, 2011. ,
DOI : 10.1007/3-540-48660-7_14
Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Recent Trends in Algebraic Development Techniques, number 7137 in Lecture Notes in Computer Science, pp.139-159, 2012. ,
DOI : 10.1007/3-540-48660-7_14
A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-6810, 1940. ,
DOI : 10.2307/2371199
Proof certificates for equality reasoning. Manuscript, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01390919
Foundational Proof Certificates in First-Order Logic, Lecture Notes in Computer Science, vol.7898, pp.24-162, 2013. ,
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485
A semantics for proof evidence In Collected abstracts of Theory and Application of Formal Proofs (LIX Colloquium 2013), pp.36-37 ,
An analysis of Girard's paradox URL: https, 1986. ,
A new paradox in type theory, Proceedings 9th Int. Congress of Logic, pp.555-570, 1991. ,
DOI : 10.1016/S0049-237X(06)80062-5
Explicit Universes for the Calculus of Constructions, Theorem Proving in Higher Order Logics, pp.115-13010, 2002. ,
DOI : 10.1007/3-540-45685-6_9
Models and proof normalization, 2009. ,
URL : https://hal.archives-ouvertes.fr/tel-00433165
Inductively defined types, Lecture Notes in Computer Science, vol.417, issue.88, pp.50-66, 1990. ,
DOI : 10.1007/3-540-52335-9_47
Functionality in Combinatory Logic, Proceedings of the National Academy of Sciences, vol.20, issue.11, pp.584-590, 1934. ,
DOI : 10.1073/pnas.20.11.584
AUTOMATH, a language for mathematics, 1968. ,
Propositional extensionality is inconsistent in Coq E-mail communication URL: https://sympa.inria.fr/sympa, pp.2013-2025, 2013. ,
Representing Control: a Study of the CPS Transformation, Mathematical Structures in Computer Science, vol.598, issue.04, pp.361-391, 1992. ,
DOI : 10.1016/0304-3975(87)90109-5
Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-7210, 2003. ,
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
Axiom of choice and complementation, Proceedings of the American Mathematical Society, pp.176-178, 1975. ,
DOI : 10.1090/S0002-9939-1975-0373893-X
Models and termination of proof-reduction in the lambda-Picalculus modulo theory ,
An inconsistent theory modulo defined by a confluent and terminating rewrite system. Manuscript URL: https://who, 2000. ,
Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003. ,
DOI : 10.1007/BFb0037116
A Machine-Checked Proof of the Odd Order Theorem, Interactive Theorem Proving, pp.163-17910, 2013. ,
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699
Some logical and syntactical observations concerning the first-order dependent type system ??P, Mathematical Structures in Computer Science, vol.9, issue.4, pp.335-359, 1999. ,
DOI : 10.1017/S0960129599002856
Logics and type systems, 1993. ,
Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, pp.39-5910, 1995. ,
DOI : 10.1007/3-540-60579-7_3
Un calcul de constructions infinies et son application a la vérification de systèmes communicants, 1996. ,
Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse de Doctorat, 1972. ,
Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987. ,
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966
An Ssreflect tutorial, Microsoft Research Inria Joint Centre, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00407778
An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00515548
Modular proof of strong normalization for the calculus of constructions, Journal of Functional Programming, vol.1, issue.2, pp.155-189, 1991. ,
A computer-checked proof of the four colour theorem, 2005. ,
Formal proof?the four-color theorem, Notices of the AMS, vol.55, issue.11, pp.1382-1393, 2008. ,
The Jordan curve theorem, formally and informally, American Mathematical Monthly, vol.114, issue.10, pp.882-894, 2007. ,
Announcement of completion URL: https://code.google.com/archive, 2014. ,
Inductive definitions: Automation and application, Higher Order Logic Theorem Proving and Its Applications, pp.200-21310, 1995. ,
DOI : 10.1007/3-540-60275-5_66
Overview, Theorem Proving in Higher Order Logics, pp.60-66 ,
DOI : 10.1007/978-1-4302-0821-1_1
URL : https://hal.archives-ouvertes.fr/in2p3-00803620
A revision of the proof of the Kepler conjecture, Discrete & Computational Geometry, vol.44, issue.1, pp.1-3410, 2010. ,
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980. ,
Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft, TAPSOFT '89, pp.241-256, 1989. ,
DOI : 10.1007/3-540-50940-2_39
Type checking with universes, Theoretical Computer Science, pp.107-13610, 1991. ,
DOI : 10.1016/0304-3975(90)90108-T
The rooster and the syntactic bracket, 19th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.169-187, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01097919
A rewrite system for strongly normalizable terms, 2015. ,
A simplification of Girard's paradox, Typed Lambda Calculi and Applications, pp.266-27810, 1995. ,
DOI : 10.1007/BFb0014058
The OpenTheory Standard Theory Library, Lecture Notes in Computer Science, vol.41, issue.1, pp.177-191, 2011. ,
DOI : 10.1007/3-540-60275-5_76
Completion of a set of rules modulo a set of equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-119410, 1986. ,
Termination of dependently typed rewrite rules, 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs), pp.257-272, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01239083
Typing in pure type systems, Information and Computation, vol.105, issue.1, pp.30-41, 1993. ,
seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009. ,
DOI : 10.1145/1629575.1629596
Scalable LCF-Style Proof Translation, Interactive Theorem Proving, pp.51-66, 2013. ,
DOI : 10.1007/978-3-642-39634-2_7
Importing HOL Light into Coq, Interactive Theorem Proving, pp.307-322 ,
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604
Réalisabilité et paramétricité dans les systèmes de types purs, 2012. ,
The CompCert C verified compiler version 2.5. Manual, Inria, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01091802
ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.386-395, 1989. ,
DOI : 10.1109/LICS.1989.39193
ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990. ,
DOI : 10.1109/LICS.1989.39193
Computation and reasoning: A type theory for computer science. Number 11 in International Series of Monographs on Computer Science, 1994. ,
Formal verification of conflict detection algorithms, International Journal on Software Tools for Technology Transfer (STTT), vol.4, issue.3, pp.371-380, 2003. ,
DOI : 10.1007/s10009-002-0084-3
An Intuitionistic Theory of Types: Predicative Part, Proceedings of the logic colloquium of Studies in logic and the foundations of mathematics, pp.73-11810, 1973. ,
DOI : 10.1016/S0049-237X(08)71945-1
Intuitionistic type theory. Notes by Giovanni Sambin of a series of lectures given in Padua, Bibliopolis Naples, 1980. ,
An intuitionistic theory of types. In Twenty-five years of constructive type theory, pp.127-172, 1998. ,
The Heterogeneous Tool Set, Hets, Tools and Algorithms for the Construction and Analysis of Systems, number 4424 in Lecture Notes in Computer Science, pp.519-522, 2007. ,
DOI : 10.1007/978-3-540-71209-1_40
Higher-order rewrite systems and their confluence, Theoretical Computer Science, vol.192, issue.1, pp.3-2910, 1998. ,
DOI : 10.1016/S0304-3975(97)00143-6
Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.342-349, 1991. ,
DOI : 10.1109/LICS.1991.151658
Programming in Martin-Löf's type theory. Number 7 in International Series of Monographs on Computer Science, 1990. ,
The HOL/NuPRL Proof Translator, Theorem Proving in Higher Order Logics, pp.329-345, 2001. ,
DOI : 10.1007/3-540-44755-5_23
Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002. ,
DOI : 10.1007/3-540-45949-9
Coinductive types and type preservation E-mail communication URL: https://sympa.inria.fr/sympa, pp.2008-2014, 2008. ,
On universes in type theory In Twenty-five years of constructive type theory, pp.191-204, 1998. ,
Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-15910, 1975. ,
DOI : 10.1016/0304-3975(75)90017-1
System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, Automated Deduction ? CADE-16, pp.202-206 ,
DOI : 10.1007/3-540-48660-7_14
Representing Isabelle in LF, Electronic Proceedings in Theoretical Computer Science, pp.85-99, 2010. ,
DOI : 10.4204/EPTCS.34.8
The MMT API: A Generic MKM System, Intelligent Computer Mathematics, number 7961 in Lecture Notes in Computer Science, pp.339-343, 2013. ,
DOI : 10.1007/978-3-642-39320-4_25
Mathematical Logic as Based on the Theory of Types, American Journal of Mathematics, vol.30, issue.3, pp.222-26210, 1908. ,
DOI : 10.2307/2369948
Towards explicit rewrite rules in the lambda-Pi-calculus modulo URL: https, IWIL -10th International Workshop on the Implementation of Logics, 2013. ,
Type checking in the lambda-Pi-calculus modulo: theory and practice, École Nationale Supérieure des Mines ,
Pure Type System conversion is always typable, Journal of Functional Programming, vol.1, issue.02, pp.153-180, 2012. ,
DOI : 10.1017/S0956796805005770
URL : https://hal.archives-ouvertes.fr/inria-00497177
The independence of Peano's fourth axiom from Martin-L??f's type theory without universes, The Journal of Symbolic Logic, vol.40, issue.03, pp.840-845, 1988. ,
DOI : 10.1007/BF01180425
A Brief Overview of HOL4, Theorem Proving in Higher Order Logics, pp.28-32978, 2008. ,
DOI : 10.1007/s00165-007-0028-5
An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf, 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, pp.150-16610, 1007. ,
DOI : 10.1007/11916277_11
Universe Polymorphism in Coq, 5th International Conference on Interactive Theorem Proving, pp.499-514, 2014. ,
DOI : 10.1007/978-3-319-08970-6_32
URL : https://hal.archives-ouvertes.fr/hal-00974721
A new type assignment for strongly normalizable terms, Computer Science Logic 2013 of Leibniz International Proceedings in Informatics (LIPIcs), pp.634-652, 2013. ,
Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic, pp.198-21210, 1967. ,
Een nadere bewijstheoretische analyse van GSTTs. Manuscript The Netherlands, 1989. ,
Confluence for abstract and higher-order rewriting, 1994. ,
By inversion, there exists B such that ? ,
By inversion, there exist A , B such that ? M : ?x : A . B and ? N : A and B {x\N } C. By principality (Definition 8.4.3), we have ?x ,
If ? A ? s and ? A ? s and A A then ?A , s such that A ?? * A and ? A ? s and s s ,
By Lemma 8.1.4, there are two cases to consider. ? If A ? A then by confluence ?A such that A By subject reduction (Lemma 8.2.8), ? A ? s ,
n . r and r r. By confluence, ?D 1 , . . . , D n such that A ?? * ?x 1 : D 1 . · · · ?x n : D n . r and A ?? * ?x 1 : D 1 . · · · ?x n : D n . r'. By subject reduction (Lemma 8.2.8), ? ?x 1 : D 1 . · · · ?x n : D n . r ? s and ? ?x 1 : D 1 . · · · ?x n : D n . r ? s . By inversion and the local minimum property ,