SICStus Prolog User"s Manual, 1993. ,
Hints in Unification, Theorem Proving in Higher Order Logics, 22nd International Conference, pp.84-98, 2009. ,
DOI : 10.1007/978-3-642-03359-9_8
The Matita Interactive Theorem Prover, pp.978-981, 2011. ,
DOI : 10.1007/978-3-642-22438-6_7
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions, Logical Methods in Computer Science, vol.8, issue.1, 2012. ,
Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, pp.1-89, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102709
Auto-validation d'un système de preuves avec familles inductives, 1999. ,
A Pragmatic Reconstruction of Lambda-Prolog, Journal of Logic Programming, 1998. ,
Canonical Big Operators, Theorem Proving in Higher Order Logics, vol.5170, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00331193
Coq development team. The Coq proof assistant reference manual. Inria, 2017. L. de Moura, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, vol.878, pp.28-43, 2012. ,
, The Lean Theorem Prover (System Description), pp.978-981, 2015.
The refined operational semantics of constraint handling rules, Logic Programming, pp.90-104, 2004. ,
ELPI: fast, Embeddable, ?Prolog Interpreter, Proceedings of LPAR, 2015. ,
Implementing HOL in an Higher Order Logic Programming Language, Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP '16, vol.4, pp.1-4, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01394686
A metaprogramming framework for formal verification, Proc. ACM Program. Lang, vol.1, pp.2475-1421, 2017. ,
Specifying theorem provers in a higher-order logic programming language, 9th International Conference on Automated Deduction, pp.61-80, 1988. ,
Encoding a dependent-type lambda-calculus in a logic programming language, Proceedings of the 10th International Conference on Automated Deduction, pp.221-235, 1990. ,
Open Proofs and Open Terms: A Basis for Interactive Logic, Computer Science Logic, 16th International Workshop, p.11, 2002. ,
, Annual Conference of the EACSL, pp.537-552, 2002.
A Machine-Checked Proof of the Odd Order Theorem, ITP, vol.7998, pp.163-179, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00816699
Type inference with algebraic universes in the Calculus of Inductive Constructions, 2005. ,
Functions-as-constructors Higher-order Unification, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), pp.1-17, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01379683
ECC, an Extended Calculus of Constructions, Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), pp.386-395, 1989. ,
Coercive Subtyping in Type Theory, Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, pp.276-296, 1996. ,
Coercive subtyping: Theory and implementation, Inf. Comput, vol.223, pp.890-5401, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01130574
Canonical Structures for the working Coq user, ITP 2013, 4th Conference on Interactive Theorem Proving, vol.7998, pp.19-34, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00816703
Type checking through unification, 2016. ,
Unification Under a Mixed Prefix, 3rd Int. Conf. Logic Programming, vol.14, pp.448-462, 1986. ,
Programming with Higher-Order Logic, p.9780521879408, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, 1991. ,
Dependently Typed Programming in Agda, Proceedings of the 6th International Conference on Advanced Functional Programming, AFP'08, pp.230-266 ,
, , pp.978-981, 2009.
Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitationàbilitationà diriger les recherches, 1996. ,
The Teyjus System-Version 2, 2015. ,
The MMT API: A Generic MKM System, Intelligent Computer Mathematics, pp.339-343, 2013. ,
Translating between implicit and explicit versions of proof, CADE-26, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01645016
Nonuniform Coercions via Unification Hints, TYPES, pp.16-29, 2009. ,
A meta-programming approach to realizing dependently typed logic programming, Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP '10, pp.187-198, 2010. ,
Une Théorie des Constructions Inductives, 1994. ,
, Theory and Practice of Logic Programming, vol.12, issue.1-2, pp.67-96, 2012.