Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. - Stefan Berghofer; Markus Wenzel 001 (TPHOLs, 1999)

Proof Terms for Simply Typed Higher Order Logic. - Stefan Berghofer; Tobias Nipkow (TPHOLs, 2000)

Executing Higher Order Logic. - Stefan Berghofer; Tobias Nipkow (TYPES, 2000)

Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts. - Christine Röckl; Daniel Hirschkoff; Stefan Berghofer (FoSSaCS, 2001)

Program Extraction in Simply-Typed Higher Order Logic. - Stefan Berghofer (TYPES, 2002)

A Constructive Proof of Higman's Lemma in Isabelle. - Stefan Berghofer (TYPES, 2003)

Extracting a formally verified, fully executable compiler from a proof assistant. - Stefan Berghofer; Martin Strecker (COCV@ETAPS, 2003)

Proofs, programs and executable specifications in higher order logic. - Stefan Berghofer (2003)

Random Testing in Isabelle/HOL. - Stefan Berghofer; Tobias Nipkow (SEFM, 2004)

Extracting a Normalization Algorithm in Isabelle/HOL. - Stefan Berghofer (TYPES, 2004)

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. - Christian Urban; Stefan Berghofer (IJCAR, 2006)

A Head-to-Head Comparison of de Bruijn Indices and Names. - Stefan Berghofer; Christian Urban (LFMTP@FLoC, 2006)

Program Extraction from Normalization Proofs. - Ulrich Berger 001; Stefan Berghofer; Pierre Letouzey; Helmut Schwichtenberg (Stud Logica, 2006)

Barendregt's Variable Convention in Rule Inductions. - Christian Urban; Stefan Berghofer; Michael Norrish (CADE, 2007)

First-Order Logic According to Fitting. - Stefan Berghofer (Arch. Formal Proofs, 2007)

POPLmark Challenge Via de Bruijn Indices. - Stefan Berghofer (Arch. Formal Proofs, 2007)

Logic-Free Reasoning in Isabelle/Isar. - Stefan Berghofer; Makarius Wenzel (AISC/MKM/Calculemus, 2008)

Nominal Inversion Principles. - Stefan Berghofer; Christian Urban (TPHOLs, 2008)

Turning Inductive into Equational Specifications. - Stefan Berghofer; Lukas Bulwahn; Florian Haftmann (TPHOLs, 2009)

Formalizing the Logic-Automaton Connection. - Stefan Berghofer; Markus Reiter (Arch. Formal Proofs, 2009)

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. - Dmitriy Traytel; Stefan Berghofer; Tobias Nipkow (APLAS, 2011)

Verification of Dependable Software using SPARK and Isabelle. - Stefan Berghofer (SSV, 2011)

Mechanizing the metatheory of LF. - Christian Urban; James Cheney; Stefan Berghofer (ACM Trans. Comput. Log., 2011)

A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL. - Stefan Berghofer (J. Autom. Reason., 2012)

The Group Law for Elliptic Curves. - Stefan Berghofer (Arch. Formal Proofs, 2017)