Stefan Berghofer

	2011
26		Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow: Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS 2011: 89-104
25		Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2): 15 (2011)
	2009
24		Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings Springer 2009
23		Stefan Berghofer, Lukas Bulwahn, Florian Haftmann: Turning Inductive into Equational Specifications. TPHOLs 2009: 131-146
22		Stefan Berghofer, Markus Reiter: Formalizing the Logic-Automaton Connection. TPHOLs 2009: 147-163
21		Stefan Berghofer, Markus Reiter: Formalizing the Logic-Automaton Connection. Archive of Formal Proofs 2009: (2009)
	2008
20		Stefan Berghofer, Makarius Wenzel: Logic-Free Reasoning in Isabelle/Isar. AISC/MKM/Calculemus 2008: 355-369
19		Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF. LICS 2008: 45-56
18		Stefan Berghofer, Christian Urban: Nominal Inversion Principles. TPHOLs 2008: 71-85
17		Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF CoRR abs/0804.1667: (2008)
	2007
16		Christian Urban, Stefan Berghofer, Michael Norrish: Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50
15		Stefan Berghofer: First-Order Logic According to Fitting. Archive of Formal Proofs 2007: (2007)
14		Stefan Berghofer: POPLmark Challenge Via de Bruijn Indices. Archive of Formal Proofs 2007: (2007)
13		Stefan Berghofer, Christian Urban: A Head-to-Head Comparison of de Bruijn Indices and Names. Electr. Notes Theor. Comput. Sci. 174(5): 53-67 (2007)
	2006
12		Christian Urban, Stefan Berghofer: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR 2006: 498-512
11		Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg: Program Extraction from Normalization Proofs. Studia Logica 82(1): 25-49 (2006)
	2004
10		Stefan Berghofer, Tobias Nipkow: Random Testing in Isabelle/HOL. SEFM 2004: 230-239
9		Stefan Berghofer: Extracting a Normalization Algorithm in Isabelle/HOL. TYPES 2004: 50-65
	2003
8		Stefan Berghofer: A Constructive Proof of Higman's Lemma in Isabelle. TYPES 2003: 66-82
7		Stefan Berghofer, Martin Strecker: Extracting a formally verified, fully executable compiler from a proof assistant. Electr. Notes Theor. Comput. Sci. 82(2): 377-394 (2003)
6		Stefan Berghofer: Proofs, programs and executable specifications in higher order logic. Technical University Munich 2003: 1-161
	2002
5		Stefan Berghofer: Program Extraction in Simply-Typed Higher Order Logic. TYPES 2002: 21-38
	2001
4		Christine Röckl, Daniel Hirschkoff, Stefan Berghofer: Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts. FoSSaCS 2001: 364-378
	2000
3		Stefan Berghofer, Tobias Nipkow: Proof Terms for Simply Typed Higher Order Logic. TPHOLs 2000: 38-52
2		Stefan Berghofer, Tobias Nipkow: Executing Higher Order Logic. TYPES 2000: 24-40
	1999
1		Stefan Berghofer, Markus Wenzel: Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. TPHOLs 1999: 19-36

Coauthor Index

1	Ulrich Berger	[11]
2	Lukas Bulwahn	[23]
3	James Cheney	[17] [19] [25]
4	Florian Haftmann	[23]
5	Daniel Hirschkoff	[4]
6	Pierre Letouzey	[11]
7	Tobias Nipkow	[2] [3] [10] [24] [26]
8	Michael Norrish	[16]
9	Markus Reiter	[21] [22]
10	Christine Röckl	[4]
11	Helmut Schwichtenberg	[11]
12	Martin Strecker	[7]
13	Dmitriy Traytel	[26]
14	Christian Urban	[12] [13] [16] [17] [18] [19] [24] [25]
15	Markus Wenzel (Makarius Wenzel)	[1] [20] [24]

Colors in the list of coauthors

Last update Sun May 27 04:04:01 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page