Benjamin Werner
Benjamin Werner
Professeur, Computer Science, Ecole Polytechnique
Verified email at polytechnique.edu - Homepage
Title
Cited by
Cited by
Year
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
335*1995
Une théorie des constructions inductives
B Werner
Université Paris-Diderot-Paris VII, 1994
3291994
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
1952011
Synthesis of ML programs in the system Coq
C Paulin-Mohring, B Werner
Journal of Symbolic Computation 15 (5-6), 607-640, 1993
1771993
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
1311993
Sets in types, types in sets
B Werner
International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997
1141997
Proof normalization modulo
G Dowek, B Werner
The Journal of Symbolic Logic 68 (04), 1289-1316, 2003
1122003
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
961999
Arithmetic as a theory modulo
G Dowek, B Werner
International Conference on Rewriting Techniques and Applications, 423-437, 2005
742005
Importing HOL light into Coq
C Keller, B Werner
International Conference on Interactive Theorem Proving, 307-322, 2010
702010
The Coq proof assistant reference manual
C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ...
Rapport Technique 177, 1995
601995
Coq in coq
B Barras, B Werner
Available on the WWW, 1997
591997
Coq en coq
B Barras
INRIA, 1996
471996
The not so simple proof-irrelevant model of CC
A Miquel, B Werner
International Workshop on Types for Proofs and Programs, 240-258, 2002
432002
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
411994
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
402006
Proof normalization modulo
G Dowek, B Werner
International Workshop on Types for Proofs and Programs, 62-77, 1998
391998
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
372007
On the strength of proof-irrelevant type theories
B Werner
International Joint Conference on Automated Reasoning, 604-618, 2006
352006
A generic normalisation proof for pure type systems
PA Mellies, B Werner
International Workshop on Types for Proofs and Programs, 254-276, 1996
321996
The system can't perform the operation now. Try again later.
Articles 1–20