Urmăriți
Benjamin Werner
Benjamin Werner
Professeur, Computer Science, Ecole Polytechnique
Adresă de e-mail confirmată pe polytechnique.edu - Pagina de pornire
Titlu
Citat de
Citat de
Anul
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
429*1995
Une théorie des constructions inductives
B Werner
Université Paris-Diderot-Paris VII, 1994
3521994
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
258*2011
Synthesis of ML programs in the system Coq
C Paulin-Mohring, B Werner
Journal of Symbolic Computation 15 (5-6), 607-640, 1993
1861993
Sets in types, types in sets
B Werner
International Symposium on Theoretical Aspects of Computer Software, 530-546, 1997
1471997
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
1401993
The Coq proof assistant reference manual
B Barras, S Boutin, C Cornes, J Courant, Y Coscoy, D Delahaye, ...
INRIA, version 6 (11), 17-21, 1999
1371999
Proof normalization modulo
G Dowek, B Werner
The Journal of Symbolic Logic 68 (04), 1289-1316, 2003
1362003
Arithmetic as a theory modulo
G Dowek, B Werner
International Conference on Rewriting Techniques and Applications, 423-437, 2005
822005
Importing HOL light into Coq
C Keller, B Werner
International Conference on Interactive Theorem Proving, 307-322, 2010
732010
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
Proof normalization modulo
G Dowek, B Werner
Types for Proofs and Programs: International Workshop, TYPES’98 Kloster …, 1999
461999
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
452003
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
441994
A generic normalisation proof for pure type systems
PA Mellies, B Werner
International Workshop on Types for Proofs and Programs, 254-276, 1996
421996
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
392006
On the strength of proof-irrelevant type theories
B Werner
Logical Methods in Computer Science 4, 2008
382008
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
Formal proofs for nonlinear optimization
X Allamigeon, S Gaubert, V Magron, B Werner
ArXiv e-prints 1404, 2014
35*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
Sistemul nu poate realiza operația în acest moment. Încercați din nou mai târziu.
Articole 1–20