| 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 | 413* | 1995 |
| Une théorie des constructions inductives B Werner Université Paris-Diderot-Paris VII, 1994 | 351 | 1994 |
| Verifying SAT and SMT in Coq for a fully automated decision procedure M Armand, G Faure, B Grégoire, C Keller, L Théry, B Werner | 253* | 2011 |
| Synthesis of ML programs in the system Coq C Paulin-Mohring, B Werner Journal of Symbolic Computation 15 (5-6), 607-640, 1993 | 183 | 1993 |
| Sets in types, types in sets B Werner International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997 | 142 | 1997 |
| 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 | 137 | 1993 |
| Proof normalization modulo G Dowek, B Werner The Journal of Symbolic Logic 68 (04), 1289-1316, 2003 | 132 | 2003 |
| The Coq proof assistant reference manual B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ... INRIA, version 6 (11), 1999 | 131 | 1999 |
| Arithmetic as a theory modulo G Dowek, B Werner International Conference on Rewriting Techniques and Applications, 423-437, 2005 | 82 | 2005 |
| Importing HOL light into Coq C Keller, B Werner International Conference on Interactive Theorem Proving, 307-322, 2010 | 73 | 2010 |
| The Coq proof assistant reference manual C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ... Rapport Technique 177, 1995 | 61 | 1995 |
| Proof normalization modulo G Dowek, B Werner Types for Proofs and Programs: International Workshop, TYPES’98 Kloster …, 1999 | 45 | 1999 |
| 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 | 45 | 1994 |
| The not so simple proof-irrelevant model of CC A Miquel, B Werner Types for Proofs and Programs: International Workshop, TYPES 2002, Berg en …, 2003 | 44 | 2003 |
| A generic normalisation proof for pure type systems PA Mellies, B Werner International Workshop on Types for Proofs and Programs, 254-276, 1996 | 42 | 1996 |
| 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 | 39 | 2006 |
| On the strength of proof-irrelevant type theories B Werner Logical Methods in Computer Science 4, 2008 | 37 | 2008 |
| 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 | 37 | 2007 |
| Formal proofs for nonlinear optimization X Allamigeon, S Gaubert, V Magron, B Werner ArXiv e-prints 1404, 2014 | 34* | 2014 |
| A normalization proof for an impredicative type system with large elimination over integers B Werner, B Nordström, K Petersson, G Plotkin International Workshop on Types for Proofs and Programs (TYPES), 341-357, 1992 | 32 | 1992 |
Christine PAULIN-MOHRINGLMF, Université Paris-Saclay在 universite-paris-saclay.fr 的电子邮件经过验证
