A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs -First International Conference, vol.7086, pp.135-150, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00639130
A Framework for Defining Computational Higher-Order Logics, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01235303
Translating HOL to Dedukti, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, vol.186, pp.74-88, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01097412
Expressing Theories in the ??-Calculus Modulo Theory and in the Dedukti System, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01441751
Mixing HOL and Coq in Dedukti, 4th Workshop on Proof eXchange for Theorem Proving, vol.186, pp.89-96, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01141789
Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, 8th International Symposium, vol.6989, pp.12-27, 2011. ,
Experimenting with Deduction Modulo, vol.6803, pp.162-176, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-01125858
Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo, LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01204701
A Rewrite System for Proof Constructivization, Proceedings of the 2016 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, vol.2, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01420634
ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti, Theoretical Aspects of Computing -ICTAC 2016 -13th International Colloquium, vol.9965, pp.459-468, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01420638
Checking Zenon Modulo Proofs in Dedukti, Proceedings 4th Workshop on Proof eXchange for Theorem Proving, vol.186, pp.57-73, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01171360
A Prototype Proof Translator from HOL to Coq, Theorem Proving in Higher Order Logics, 13th International Conference, vol.1869, pp.108-125, 2000. ,
Matching concepts across HOL libraries, Intelligent Computer Mathematics -International Conference, CICM 2014, Coimbra, Portugal, vol.8543, pp.267-281, 2014. ,
Representing Model Theory in a Type-Theoretical Logical Framework, Theoretical Computer Science, vol.412, pp.4919-4945, 2011. ,
Importing Mathematics from HOL into Nuprl, Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, vol.1125, pp.267-281, 1996. ,
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Certified Programs and Proofs -Third International Conference, vol.8307, pp.131-146, 2013. ,
The OpenTheory Standard Theory Library, NASA Formal MethodsThird International Symposium, NFM 2011, vol.6617, pp.177-191, 2011. ,
Scalable LCF-Style Proof Translation, Interactive Theorem Proving, number 7998 in LNCS, pp.51-66, 2013. ,
Importing HOL Light into Coq, ITP, number 6172 in LNCS, pp.307-322, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00520604
Foundational Proof Certificates: Making Proof Universal and Permanent, Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, pp.1-2, 2013. ,
FoCaLiZe: Inside an F-IDE, Proceedings 1st Workshop on Formal Integrated Development Environment, vol.149, pp.64-78, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01203501
Making proofs in a hierarchy of mathematical structures, Proceedings of Calculemus, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01531083
Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, MINES Paritech, 2015. ,
An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf, Logic for Programming, Artificial Intelligence, and Reasoning, number 4246 in LNCS, pp.150-166, 2006. ,
Encoding the HOL Light logic in Coq, 2007. ,
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01152588