Distilling abstract machines, Proceedings of the 19th International conference on Functional programming, pp.363-376, 2014. ,
DOI : 10.1145/2628136.2628154
Hints in Unification, Theorem Proving in Higher Order Logics, 22nd International Conference Proceedings, pp.84-98, 2009. ,
DOI : 10.1007/BFb0028402
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions, Logical Methods in Computer Science, vol.2, issue.1, p.2012 ,
DOI : 10.1007/s001650200018
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, pp.64-69, 2011. ,
DOI : 10.1007/3-540-48256-3_12
URL : http://www.msr-inria.inria.fr/%7Egares/system_description2011.pdf
Auto-validation d'un système de preuves avec familles inductives, Thèse de doctorat, 1999. ,
A Pragmatic Reconstruction of Lambda-Prolog, Journal of Logic Programming, 1998. ,
The lambda-Pi-calculus Modulo as a Universal Proof Language, Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving CEUR Workshop Proceedings, pp.28-43, 2012. ,
Sidi Ould Biha, and Ioana Pasca. Canonical Big Operators, Theorem Proving in Higher Order Logics, 2008. ,
The Complexity of Equivariant Unification, pp.332-344, 2004. ,
DOI : 10.1007/978-3-540-27836-8_30
Nonuniform Coercions via Unification Hints, TYPES, pp.16-29, 2009. ,
DOI : 10.1007/978-3-540-71067-7_23
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, pp.1-410, 2016. ,
DOI : 10.1007/978-3-642-22673-1_18
URL : https://hal.archives-ouvertes.fr/hal-01394686
ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter, Proceedings of LPAR, 2015. ,
DOI : 10.1007/978-3-662-48899-7_32
Elaboration in Dependent Type Theory, 1505. ,
Constraint Handling Rules, 2009. ,
A Machine-Checked Proof of the Odd Order Theorem, ITP, pp.163-179, 2013. ,
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699
The Abella Interactive Theorem Prover (System Description), Proceedings of IJCAR 2008, pp.154-161, 2008. ,
DOI : 10.1007/978-3-540-71070-7_13
URL : http://arxiv.org/pdf/0803.2305v2.pdf
Open Proofs and Open Terms: A Basis for Interactive Logic In Computer Science Logic, 16th International Workshop, CSL, 11th Annual Conference of the EACSL Proceedings, pp.537-552, 2002. ,
Nominal abstraction. Information and Computation, pp.48-73, 2011. ,
DOI : 10.1016/j.ic.2010.09.004
URL : https://doi.org/10.1016/j.ic.2010.09.004
Type inference with algebraic universes in the Calculus of Inductive Constructions, 2005. ,
A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, vol.6, issue.3, pp.199-207, 2007. ,
DOI : 10.1093/comjnl/6.4.308
URL : https://hal.archives-ouvertes.fr/hal-00154508
Coercive subtyping: Theory and implementation, Information and Computation, vol.223, pp.18-42, 2013. ,
DOI : 10.1016/j.ic.2012.10.020
URL : https://hal.archives-ouvertes.fr/hal-01130574
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
URL : ftp://ftp.dcs.ed.ac.uk/pub/lego/lics89.ps.Z
Coercive subtyping in type theory, Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, pp.276-296, 1996. ,
DOI : 10.1007/3-540-63172-0_45
URL : http://www.dur.ac.uk/CARG/papers/SUBTYPING96.ps.gz
Type checking throug unification. CoRR, abs, 1609. ,
A logic programming language with lambda-abstraction, function variables, and simple unification, pp.253-281, 1991. ,
Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992. ,
DOI : 10.1016/0747-7171(92)90011-R
Higher-order logic programming, 3rd Int. Conf. Logic Programming, pp.448-462, 1986. ,
DOI : 10.1007/3-540-16492-8_94
URL : https://hal.archives-ouvertes.fr/hal-00776197
Programming with Higher-Order Logic, 2012. ,
DOI : 10.1017/cbo9781139021326
URL : https://hal.archives-ouvertes.fr/hal-00776197
Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, p.51, 1991. ,
DOI : 10.1016/0168-0072(91)90068-W
Dependently Typed Programming in Agda, Proceedings of the 6th International Conference on Advanced Functional Programming, AFP'08, pp.230-266, 2009. ,
DOI : 10.1145/1481861.1481862
Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitationàbilitationà diriger les recherches, 1996. ,
The MMT API: A Generic MKM System, pp.339-343, 2013. ,
DOI : 10.1007/978-3-642-39320-4_25
URL : http://arxiv.org/pdf/1306.3199
Translating between implicit and explicit versions of proof, 2017. ,
Une Théorie des Constructions Inductives, 1994. ,
The Language Features and Architecture of B-prolog. Theory Pract, Log. Program, vol.12, issue.12, pp.189-218, 2012. ,