Follow
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
400*1995
Une théorie des constructions inductives
B Werner
Université Paris-Diderot-Paris VII, 1994
3501994
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
1811993
Sets in types, types in sets
B Werner
International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997
1371997
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
1371993
Proof normalization modulo
G Dowek, B Werner
The Journal of Symbolic Logic 68 (04), 1289-1316, 2003
1262003
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 1999
1261999
Arithmetic as a theory modulo
G Dowek, B Werner
International Conference on Rewriting Techniques and Applications, 423-437, 2005
792005
Importing HOL light into Coq
C Keller, B Werner
International Conference on Interactive Theorem Proving, 307-322, 2010
722010
The Coq proof assistant reference manual
C Cornes, J Courant, JC Filliâtre, G Huet, P Manoury, C Paulin-Mohring, ...
Rapport Technique 177, 1995
621995
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
432003
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
421994
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
412006
Proof normalization modulo
G Dowek, B Werner
Types for Proofs and Programs: International Workshop, TYPES’98 Kloster …, 1999
401999
A generic normalisation proof for pure type systems
PA Mellies, B Werner
International Workshop on Types for Proofs and Programs, 254-276, 1996
401996
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
Logical Methods in Computer Science 4, 2008
362008
Formal proofs for nonlinear optimization
X Allamigeon, S Gaubert, V Magron, B Werner
ArXiv e-prints 1404, 2014
33*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
321992
The system can't perform the operation now. Try again later.
Articles 1–20