| The COQ Proof assistant, Reference Manual, Version 5.10 C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Munoz, C Murthy, ... INRIA, 1995 | 345* | 1995 |
| Une théorie des constructions inductives B Werner Université Paris-Diderot-Paris VII, 1994 | 336 | 1994 |
| A modular integration of SAT/SMT solvers to Coq through proof witnesses M Armand, G Faure, B Grégoire, C Keller, L Théry, B Werner International Conference on Certified Programs and Proofs, 135-150, 2011 | 208 | 2011 |
| Synthesis of ML programs in the system Coq C Paulin-Mohring, B Werner Journal of Symbolic Computation 15 (5-6), 607-640, 1993 | 179 | 1993 |
| The Coq proof assistant user's guide: version 5.8 G Dowek, A Felty, H Herbelin, G Huet, C Parent, C Paulin-Mohring, ... INRIA, 1993 | 134 | 1993 |
| Sets in types, types in sets B Werner International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997 | 125 | 1997 |
| Proof normalization modulo G Dowek, B Werner The Journal of Symbolic Logic 68 (04), 1289-1316, 2003 | 116 | 2003 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 108 | 1999 |
| Importing HOL light into Coq C Keller, B Werner International Conference on Interactive Theorem Proving, 307-322, 2010 | 73 | 2010 |
| Arithmetic as a theory modulo G Dowek, B Werner International Conference on Rewriting Techniques and Applications, 423-437, 2005 | 72 | 2005 |
| The Coq proof assistant reference manual C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ... Rapport Technique 177, 1995 | 62 | 1995 |
| Coq in coq B Barras, B Werner Available on the WWW, 1997 | 59 | 1997 |
| The not so simple proof-irrelevant model of CC A Miquel, B Werner International Workshop on Types for Proofs and Programs, 240-258, 2002 | 44 | 2002 |
| A computational approach to pocklington certificates in type theory B Grégoire, L Théry, B Werner International Symposium on Functional and Logic Programming, 97-113, 2006 | 41 | 2006 |
| On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study H Geuvers, B Werner Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, 320-329, 1994 | 41 | 1994 |
| Proof normalization modulo G Dowek, B Werner International Workshop on Types for Proofs and Programs, 62-77, 1998 | 39 | 1998 |
| Simple types in type theory: Deep and shallow encodings F Garillot, B Werner International Conference on Theorem Proving in Higher Order Logics, 368-382, 2007 | 38 | 2007 |
| A generic normalisation proof for pure type systems PA Mellies, B Werner International Workshop on Types for Proofs and Programs, 254-276, 1996 | 37 | 1996 |
| On the strength of proof-irrelevant type theories B Werner Logical Methods in Computer Science 4, 2008 | 35 | 2008 |
| A normalization proof for an impredicative type system with large elimination over integers B Werner International Workshop on Types for Proofs and Programs (TYPES), 341-357, 1992 | 33 | 1992 |
Christine PAULIN-MOHRINGLMF, Université Paris-SaclayVerified email at universite-paris-saclay.fr
