Stefan Berghofer

29 papers A* 1A 2B 3Journal 8Unranked 13
YearRankTypeTitle / Venue / Authors
2017 J jnl
The Group Law for Elliptic Curves.
Arch. Formal Proofs
Stefan Berghofer
2012 J jnl
A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL.
J. Autom. Reason.
Stefan Berghofer
2011 B conf
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.
APLAS
Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow
2011 J jnl
Mechanizing the metatheory of LF.
ACM Trans. Comput. Log.
Christian Urban, James Cheney, Stefan Berghofer
2011 — conf
Verification of Dependable Software using SPARK and Isabelle.
SSV
Stefan Berghofer
2009 — conf
Formalizing the Logic-Automaton Connection.
TPHOLs
Stefan Berghofer, Markus Reiter
2009 J jnl
Formalizing the Logic-Automaton Connection.
Arch. Formal Proofs
Stefan Berghofer, Markus Reiter
2009 — ed.
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
TPHOLs
Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel
2009 — conf
Turning Inductive into Equational Specifications.
TPHOLs
Stefan Berghofer, Lukas Bulwahn, Florian Haftmann
2008 — conf
Logic-Free Reasoning in Isabelle/Isar.
AISC/MKM/Calculemus
Stefan Berghofer, Makarius Wenzel
2008 J jnl
Mechanizing the Metatheory of LF
CoRR
Christian Urban, James Cheney, Stefan Berghofer
2008 A* conf
Mechanizing the Metatheory of LF.
LICS
Christian Urban, James Cheney, Stefan Berghofer
2008 — conf
Nominal Inversion Principles.
TPHOLs
Stefan Berghofer, Christian Urban
2007 A conf
Barendregt's Variable Convention in Rule Inductions.
CADE
Christian Urban, Stefan Berghofer, Michael Norrish
2007 J jnl
First-Order Logic According to Fitting.
Arch. Formal Proofs
Stefan Berghofer
2007 J jnl
POPLmark Challenge Via de Bruijn Indices.
Arch. Formal Proofs
Stefan Berghofer
2006 — conf
A Head-to-Head Comparison of de Bruijn Indices and Names.
LFMTP@FLoC
Stefan Berghofer, Christian Urban
2006 A conf
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
IJCAR
Christian Urban, Stefan Berghofer
2006 J jnl
Program Extraction from Normalization Proofs.
Stud Logica
Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg
2004 — conf
Extracting a Normalization Algorithm in Isabelle/HOL.
TYPES
Stefan Berghofer
2004 B conf
Random Testing in Isabelle/HOL.
SEFM
Stefan Berghofer, Tobias Nipkow
2003 — conf
A Constructive Proof of Higman's Lemma in Isabelle.
TYPES
Stefan Berghofer
2003 — conf
Extracting a formally verified, fully executable compiler from a proof assistant.
COCV
Stefan Berghofer, Martin Strecker
2003 — —
Proofs, programs and executable specifications in higher order logic.
Stefan Berghofer
2002 — conf
Program Extraction in Simply-Typed Higher Order Logic.
TYPES
Stefan Berghofer
2001 B conf
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.
FoSSaCS
Christine Röckl, Daniel Hirschkoff, Stefan Berghofer
2000 — conf
Executing Higher Order Logic.
TYPES
Stefan Berghofer, Tobias Nipkow
2000 — conf
Proof Terms for Simply Typed Higher Order Logic.
TPHOLs
Stefan Berghofer, Tobias Nipkow
1999 — conf
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.
TPHOLs
Stefan Berghofer, Markus Wenzel