Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, 8th International Conference Proceedings. Volume 4583 of Lecture Notes in Computer Science, pp.102-117, 2007. ,
DOI : 10.1007/978-3-540-73228-0_9
The OpenTheory Standard Theory Library, Third International Symposium on NASA Formal Methods, pp.177-191, 2011. ,
DOI : 10.1007/3-540-60275-5_76
URL : http://www.gilith.com/research/papers/stdlib.pdf
Engineering mathematics: the odd order theorem proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.1-2, 2013. ,
DOI : 10.1145/2429069.2429071
FoCaLiZe and Dedukti to the Rescue for Proof Interoperability ,
DOI : 10.1007/11916277_11
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique), p.7, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01299180
An analysis of girard's paradox, LICS, IEEE Computer Society, pp.227-236, 1986. ,
An introduction to mathematical logic and type theory -to truth through proof. Computer science and applied mathematics, 1986. ,
DOI : 10.1007/978-94-015-9934-4