Papers of Stefan Berghofer

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. © Springer-Verlag 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 Formal-Logic 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. © Springer-Verlag 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. © Springer-Verlag 2000. Available as ps, pdf, dvi, slides available as pdf, ps.
• Christine Röckl and Daniel Hirschkoff and Stefan Berghofer. Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the Pi-Calculus and Mechanizing the Theory of Contexts. In Proc. FOSSACS'01, LNCS 2030. © Springer-Verlag 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. © Springer-Verlag 2002. Available as ps, pdf, dvi.
• Stefan Berghofer. Program Extraction in simply-typed Higher Order Logic. In H. Geuvers and F. Wiedijk, editors, Types for Proofs and Programs, International Workshop, (TYPES 2002), LNCS 2646. © Springer-Verlag 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. © Springer-Verlag 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. © Springer-Verlag 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. © Springer-Verlag 2006. Available as pdf.
• Stefan Berghofer and Christian Urban. A Head-to-Head Comparison of de Bruijn Indices and Names. In Brigitte Pientka and Alberto Momigliano, editors, International Workshop on Logical Frameworks and Meta-Languages: 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 (CADE-21), LNCS. © Springer-Verlag 2007. Available as pdf.
• Christian Urban, James Cheney and Stefan Berghofer. Mechanising the Metatheory of LF. In Frank Pfenning, editor, Twenty-Third 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 Ait-Mohamed and César Muñoz, editor, 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS 5170. © Springer-Verlag 2008. Available as pdf.
• Stefan Berghofer and Markus Wenzel. Logic-free 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. © Springer-Verlag 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. © Springer-Verlag 2009. Available as pdf.
• Stefan Berghofer and Markus Reiter. Formalizing the Logic-Automaton 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. © Springer-Verlag 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 - Leibniz-Zentrum für Informatik, 2012.
• Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow. Extending Hindley-Milner 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

• Stefan Berghofer and Tobias Nipkow. Random testing in Isabelle/HOL. In Jorge R. Cuellar and Zhiming Liu, editors, 2nd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2004), IEEE Computer Society Press 2004. Available as ps, pdf.
• Ulrich Berger, Stefan Berghofer, Pierre Letouzey and Helmut Schwichtenberg. Program Extraction from Normalization Proofs. Studia Logica, 82:25-49. © Springer-Verlag 2006. Available as pdf. See also the corresponding Isabelle theories.

Formal Proof Developments

• Stefan Berghofer. First-Order Logic According to Fitting. Archive of Formal Proofs, August 2007.
• Stefan Berghofer. The Group Law for Elliptic Curves. Archive of Formal Proofs, February 2017.

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, Jouy-en-Josas, 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 Curry-Howard 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 Logic-Automaton Connection. Talk given at Seminar of the Programming for Multicore Architectures Research Center, Uppsala, Sweden, April 2009.
• Formalizing the Logic-Automaton 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 Security-Critical Software with SPARK/Ada at secunet. Invited talk given at Frama-C & SPARK Day 2017, Paris, France, May 2017.