Decidability of conversion for type theory in type theory, PACMPL, vol.2, p.29, 2018. ,
Type theory in type theory using quotient inductive types, vol.16, pp.18-29, 2016. ,
Revisiting Parametricity: Inductives and Uniformity of Propositions, CoqPL'18, 2018. ,
CertiCoq: A verified compiler for Coq, 2017. ,
Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00502496
Auto-validation d'un système de preuves avec familles inductives, vol.7, 1999. ,
Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, issue.2, pp.107-152, 2012. ,
The next 700 syntactical models of type theory, CPP'17, pp.182-194, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
Type Theory Should Eat Itself, Electronic Notes in Theoretical Computer Science, vol.228, pp.21-36, 2008. ,
Certified Programming with Dependent Types, Introduction to algorithms, 2009. ,
Typed syntactic meta-programming, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ACM, ICFP '13, 2013. ,
A Metaprogramming Framework for Formal Verification, Proceedings of the 22st ACM SIGPLAN Conference on Functional Programming, vol.34, p.29, 2017. ,
Verified Extraction from Coq to a Lambda-Calculus, Coq Workshop, 2016. ,
A certifying extraction with time bounds from coq to call-byvalue ?-calculus, p.11818, 1904. ,
Weak call-by-value lambda calculus as a model of computation in Coq, pp.189-206, 2017. ,
The rooster and the syntactic bracket, 19th International Conference on Types for Proofs and Programs, TYPES 2013, vol.26, pp.169-187, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01097919
The definitional side of the forcing, LICS'16, pp.367-376, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01319066
Programming in the ?-calculus: From Church to Scott and back, The Beauty of Functional Code, vol.8106, pp.168-180, 2013. ,
Parametricity in an impredicative sort, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00730913
Canonicity of Weak ?-groupoid Laws Using Parametricity Theory, Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01105252
Extensible and efficient automation through reflective tactics, ESOP 2016, 2016. ,
Extensible proof engineering in intensional type theory, 2014. ,
Efficient self-interpretations in lambda calculus, J Funct Program, vol.2, issue.3, pp.345-363, 1992. ,
OEuf: minimizing the coq extraction TCB, Proceedings of CPP 2018, pp.172-185, 2018. ,
An effectful way to eliminate addiction to dependence, LICS'17, pp.1-12, 2017. ,
Types, abstraction and parametric polymorphism, pp.513-523, 1983. ,
Template meta-programming for haskell, SIGPLAN Not, vol.37, issue.12, pp.60-75, 2002. ,
Template meta-programming for haskell, Proceedings of the, pp.1-16, 2002. ,
Program-ing Finger Trees in Coq, pp.13-24, 2007. ,
Multi-stage programming with explicit annotations, pp.203-217, 1997. ,
Theorems for free! In: Functional Programming Languages and Computer Architecture, pp.347-359, 1989. ,
Engineering Proof by Reflection in Agda, Implementation and Application of Functional Languages, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00987610
Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading, Journal of Functional Programming, vol.27, p.10, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01671925
Mtac: A Monad for Typed Tactic Programming in Coq, Journal of Functional Programming, vol.25, 2015. ,