Stefan Berghofer

Publication Activity (10 Years)

Years Active: 1999-2017
Publications (10 Years): 1

Top Venues

Arch. Formal Proofs

J. Autom. Reason.

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Stefan Berghofer
The Group Law for Elliptic Curves. Arch. Formal Proofs 2017 (2017)
Stefan Berghofer
A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL. J. Autom. Reason. 49 (3) (2012)
Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS (2011)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12 (2) (2011)
Stefan Berghofer
Verification of Dependable Software using SPARK and Isabelle. SSV (2011)
Stefan Berghofer, Markus Reiter
Formalizing the Logic-Automaton Connection. TPHOLs (2009)
Stefan Berghofer, Lukas Bulwahn, Florian Haftmann
Turning Inductive into Equational Specifications. TPHOLs (2009)
Stefan Berghofer, Markus Reiter
Formalizing the Logic-Automaton Connection. Arch. Formal Proofs 2009 (2009)
Stefan Berghofer, Christian Urban
Nominal Inversion Principles. TPHOLs (2008)
Stefan Berghofer, Makarius Wenzel
Logic-Free Reasoning in Isabelle/Isar. AISC/MKM/Calculemus (2008)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the Metatheory of LF CoRR (2008)
Christian Urban, James Cheney, Stefan Berghofer
Mechanizing the Metatheory of LF. LICS (2008)
Christian Urban, Stefan Berghofer, Michael Norrish
Barendregt's Variable Convention in Rule Inductions. CADE (2007)
Stefan Berghofer
First-Order Logic According to Fitting. Arch. Formal Proofs 2007 (2007)
Stefan Berghofer, Christian Urban
A Head-to-Head Comparison of de Bruijn Indices and Names. Electron. Notes Theor. Comput. Sci. 174 (5) (2007)
Stefan Berghofer
POPLmark Challenge Via de Bruijn Indices. Arch. Formal Proofs 2007 (2007)
Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg
Program Extraction from Normalization Proofs. Stud Logica 82 (1) (2006)
Christian Urban, Stefan Berghofer
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR (2006)
Stefan Berghofer, Tobias Nipkow
Random Testing in Isabelle/HOL. SEFM (2004)
Stefan Berghofer
Extracting a Normalization Algorithm in Isabelle/HOL. TYPES (2004)
Stefan Berghofer, Martin Strecker
Extracting a formally verified, fully executable compiler from a proof assistant. Electron. Notes Theor. Comput. Sci. 82 (2) (2003)
Stefan Berghofer
A Constructive Proof of Higman's Lemma in Isabelle. TYPES (2003)
Stefan Berghofer
Program Extraction in Simply-Typed Higher Order Logic. TYPES (2002)
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)
Stefan Berghofer, Tobias Nipkow
Proof Terms for Simply Typed Higher Order Logic. TPHOLs (2000)
Stefan Berghofer, Tobias Nipkow
Executing Higher Order Logic. TYPES (2000)
Stefan Berghofer, Markus Wenzel
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. TPHOLs (1999)

Stefan Berghofer.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Stefan Berghofer