Benjamin Werner

	2011
18		Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP 2011: 135-150
17		Gyesik Lee, Benjamin Werner: Proof-irrelevant model of CC with predicative induction and judgmental equality Logical Methods in Computer Science 7(4): (2011)
	2010
16		Chantal Keller, Benjamin Werner: Importing HOL Light into Coq. ITP 2010: 307-322
	2008
15		Benjamin Werner: On the strength of proof-irrelevant type theories CoRR abs/0808.3928: (2008)
14		Benjamin Werner: On the Strength of Proof-irrelevant Type Theories. Logical Methods in Computer Science 4(3): (2008)
	2007
13		François Garillot, Benjamin Werner: Simple Types in Type Theory: Deep and Shallow Encodings. TPHOLs 2007: 368-382
	2006
12		Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers Springer 2006
11		Benjamin Grégoire, Laurent Théry, Benjamin Werner: A Computational Approach to Pocklington Certificates in Type Theory. FLOPS 2006: 97-113
10		Benjamin Werner: On the Strength of Proof-Irrelevant Type Theories. IJCAR 2006: 604-618
	2005
9		Gilles Dowek, Benjamin Werner: Arithmetic as a Theory Modulo. RTA 2005: 423-437
	2004
8		Martín Abadi, Georges Gonthier, Benjamin Werner: Choice in Dynamic Linking. FoSSaCS 2004: 12-26
	2003
7		Gilles Dowek, Benjamin Werner: Proof normalization modulo. J. Symb. Log. 68(4): 1289-1316 (2003)
	2002
6		Alexandre Miquel, Benjamin Werner: The Not So Simple Proof-Irrelevant Model of CC. TYPES 2002: 240-258
	1998
5		Gilles Dowek, Benjamin Werner: Proof Normalization Modulo. TYPES 1998: 62-77
	1997
4		Benjamin Werner: Sets in Types, Types in Sets. TACS 1997: 530-346
	1996
3		Paul-André Melliès, Benjamin Werner: A Generic Normalisation Proof for Pure Type Systems. TYPES 1996: 254-276
	1994
2		Herman Geuvers, Benjamin Werner: On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study LICS 1994: 320-329
	1993
1		Christine Paulin-Mohring, Benjamin Werner: Synthesis of ML Programs in the System Coq. J. Symb. Comput. 15(5/6): 607-640 (1993)

Coauthor Index

1	Martín Abadi	[8]
2	Michaël Armand	[18]
3	Gilles Dowek	[5] [7] [9]
4	Germain Faure	[18]
5	Jean-Christophe Filliâtre	[12]
6	François Garillot	[13]
7	Herman Geuvers	[2]
8	Georges Gonthier	[8]
9	Benjamin Grégoire	[11] [18]
10	Chantal Keller	[16] [18]
11	Gyesik Lee	[17]
12	Paul-André Melliès	[3]
13	Alexandre Miquel	[6]
14	Christine Paulin-Mohring	[1] [12]
15	Laurent Théry	[11] [18]

Colors in the list of coauthors

Last update Sat Feb 11 22:55:45 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page