
Papers of Stefan Berghofer
See also DBLP.
Journal Articles
 Stefan Berghofer.
A Solution to the POPLmark Challenge using de Bruijn indices in Isabelle/HOL.
In Stephanie Weirich and Benjamin Pierce, editors,
Special issue on the POPLmark challenge, Journal of Automated Reasoning.
© SpringerVerlag 2011.
The final publication is available at www.springerlink.com.
Author's version available as pdf,
slides available as pdf,
theory files available from the Archive of Formal Proofs.
Conference Papers
 Stefan Berghofer and Markus Wenzel.
Inductive datatypes in HOL  lessons learned in FormalLogic Engineering.
In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Théry, editors,
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99,
LNCS 1690. © SpringerVerlag 1999.
Available as
ps, pdf,
dvi, slides available as pdf,
ps.
 Stefan Berghofer and Tobias Nipkow.
Proof terms for simply typed higher order logic.
In J. Harrison and M. Aagaard, editors,
Theorem Proving in Higher Order Logics,
13th International Conference, TPHOLs 2000,
LNCS 1869. © SpringerVerlag 2000.
Available as
ps, pdf,
dvi, slides available as pdf,
ps.
 Christine Röckl and
Daniel Hirschkoff and Stefan Berghofer.
HigherOrder Abstract Syntax with Induction in Isabelle/HOL:
Formalizing the PiCalculus and Mechanizing the Theory of Contexts.
In Proc. FOSSACS'01,
LNCS 2030.
© SpringerVerlag 2001. Available as
ps.
 Stefan Berghofer and Tobias Nipkow.
Executing Higher Order Logic.
In P. Callaghan, Z. Luo, J. McKinna, R. Pollack, editors,
Types for Proofs and Programs, International Workshop, (TYPES 2000),
LNCS 2277. © SpringerVerlag 2002.
Available as
ps, pdf,
dvi.
 Stefan Berghofer.
Program Extraction in simplytyped Higher Order Logic.
In H. Geuvers and F. Wiedijk, editors,
Types for Proofs and Programs, International Workshop, (TYPES 2002),
LNCS 2646. © SpringerVerlag 2003.
Available as
ps, pdf.
 Stefan Berghofer.
A constructive proof of Higman's lemma in Isabelle.
In S. Berardi and M. Coppo, editors,
Types for Proofs and Programs, International Workshop, (TYPES 2003),
LNCS 3085. © SpringerVerlag 2004.
Available as
ps, pdf.
 Stefan Berghofer.
Extracting a normalization algorithm in Isabelle/HOL.
In J.C. Filliâtre, C. Paulin and B. Werner, editors,
Types for Proofs and Programs, International Workshop, (TYPES 2004),
LNCS 3839. © SpringerVerlag 2005.
Available as
pdf.
 Christian Urban and Stefan Berghofer.
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
In Ulrich Furbach and Natarajan Shankar, editors,
Third International Joint Conference on Automated Reasoning (IJCAR 2006),
LNCS 4130. © SpringerVerlag 2006.
Available as
pdf.
 Stefan Berghofer and Christian Urban.
A HeadtoHead Comparison of de Bruijn Indices and Names.
In Brigitte Pientka and Alberto Momigliano, editors,
International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice
(LFMTP'06),
Volume 174, Issue 5 of ENTCS.
© Elsevier 2006.
Available as pdf.
 Christian Urban, Stefan Berghofer
and Michael Norrish.
Barendregt's Variable Convention in Rule Inductions.
In Frank Pfenning, editor,
21st International Conference on Automated Deduction (CADE21),
LNCS. © SpringerVerlag 2007.
Available as pdf.
 Christian Urban,
James Cheney
and Stefan Berghofer.
Mechanising the Metatheory of LF.
In Frank Pfenning, editor,
TwentyThird Annual IEEE Symposium on Logic in Computer Science (LICS 2008),
IEEE Computer Society Press 2008.
Extended technical report and Isabelle theory files available here.
 Stefan Berghofer and Christian Urban.
Nominal Inversion Principles.
In Sofiène Tahar, Otmane AitMohamed and César Muñoz, editor,
21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008),
LNCS 5170. © SpringerVerlag 2008.
Available as pdf.
 Stefan Berghofer and Markus Wenzel.
Logicfree reasoning in Isabelle/Isar.
In Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki and Freek Wiedijk, editor,
7th International Conference on Mathematical Knowledge Management,
LNCS 5144. © SpringerVerlag 2008.
Available as pdf.
 Stefan Berghofer, Lukas Bulwahn
and Florian Haftmann.
Turning inductive into equational specifications.
In Stefan Berghofer, Tobias Nipkow, Christian Urban and Markus Wenzel, editor,
22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009),
LNCS 5674. © SpringerVerlag 2009.
Available as pdf.
 Stefan Berghofer and Markus Reiter.
Formalizing the LogicAutomaton Connection.
In Stefan Berghofer, Tobias Nipkow, Christian Urban and Markus Wenzel, editors,
22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009),
LNCS 5674. © SpringerVerlag 2009.
Available as pdf,
slides available as pdf,
theory files available from the Archive of Formal Proofs.
 Stefan Berghofer.
Verification of Dependable Software using SPARK and Isabelle.
In Jörg Brauer, Marco Roveri and Hendrik Tews, editors,
6th International Workshop on Systems Software Verification (SSV 2011).
Available as pdf.
Also appeared in OASICS Volume 24,
Schloss Dagstuhl  LeibnizZentrum für Informatik, 2012.
 Dmitriy Traytel, Stefan Berghofer,
Tobias Nipkow.
Extending HindleyMilner Type Inference with Coercive Structural Subtyping.
In Hongseok Yang, editor,
Ninth Asian Symposium on Programming Languages and Systems (APLAS 2011).
Paper and slides available here.
Invited Papers
Formal Proof Developments
Theses
 Stefan Berghofer.
Proofs, Programs and Executable Specifications in
Higher Order Logic. Ph.D. thesis, Institut für Informatik,
Technische Universität München, 2003.
Also available as ps, official version available
here.
 Stefan Berghofer.
Definitorische Konstruktion induktiver Datentypen in Isabelle/HOL.
Master's thesis, Institut für Informatik, Technische Universität
München, 1998.
Available as ps, pdf,
dvi, slides available as ps.
Slides of talks
 New features of the Isabelle theorem prover 
proof terms and code generation. System demonstration given at
Types Working Group Annual
Meeting 2000, Durham, UK, December 2000.
 Executing Higher Order Logic. Talk given
at Deduction
Seminar, Dagstuhl, March 2001.
 Program extraction in Isabelle.
Talk given at
TYPES 2002 Workshop, Berg en Dal, Netherlands, April 2002.
 A constructive proof of Higman's
lemma in Isabelle.
Talk given at
TYPES 2003 Workshop, Torino, Italy, May 2003.
 Program extraction from a proof of
weak normalization.
Talk given at
TYPES 2004 Workshop, JouyenJosas, France, December 2004.
 A solution to the PoplMark challenge in Isabelle/HOL.
Talk given at
TYPES 2006 Workshop, Nottingham, UK, April 2006.
 Proof terms in Isabelle.
Talk given at Small TYPES workshop
on CurryHoward Implementation Techniques, Nijmegen, Netherlands, December 2006.
 Nominal Datatypes in Isabelle/HOL.
Talk given at TYPES 2007
Conference, Cividale, Italy, May 2007.
 Nominal Inversion Principles.
Talk given at TYPES 2008
Conference, Torino, Italy, March 2008.
 Implementation of a Coherent Logic Prover for Isabelle.
Talk given at Automating Coherent Logic Seminar,
Oslo, Norway, June 2008.
 Formalizing the LogicAutomaton Connection.
Talk given at Seminar
of the Programming for Multicore Architectures Research Center, Uppsala, Sweden, April 2009.
 Formalizing the LogicAutomaton Connection.
Keynote talk given at Workshop
on Algebraic computing, soft computing, and program verification, Castro Urdiales, Spain,
April 2010.
 Verification of Dependable Software using SPARK and Isabelle.
Invited talk given at SPARK
User Group 2012, Bath, UK, November 2012.
 Development of SecurityCritical Software with SPARK/Ada at secunet.
Invited talk given at FramaC & SPARK Day 2017, Paris, France, May 2017.
Last modified: Fri Jun 09 23:35:08 CEST 2017
