עקוב אחר
Benjamin Werner
Benjamin Werner
Professeur, Computer Science, Ecole Polytechnique
כתובת אימייל מאומתת בדומיין polytechnique.edu - דף הבית
כותרת
צוטט על ידי
צוטט על ידי
שנה
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‏
430*1995
Une théorie des constructions inductives‏
B Werner‏
Université Paris-Diderot-Paris VII, 1994‏
3531994
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
המערכת אינה יכולה לבצע את הפעולה כעת. נסה שוב מאוחר יותר.
מאמרים 1–20