Stefan Berghofer - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 27 from 27

2017

The Group Law for Elliptic CurvesStefan Berghofer. afp, 2017, 2017. [doi]

2012

A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOLStefan Berghofer. JAR, 49(3):303-326, 2012. [doi]

2011

Verification of Dependable Software using SPARK and IsabelleStefan Berghofer. ssv 2012: 15-31 [doi]

Extending Hindley-Milner Type Inference with Coercive Structural SubtypingDmitriy Traytel, Stefan Berghofer, Tobias Nipkow. aplas 2011: 89-104 [doi]

Mechanizing the metatheory of LFChristian Urban, James Cheney, Stefan Berghofer. tocl, 12(2):15, 2011. [doi]

2009

Turning Inductive into Equational SpecificationsStefan Berghofer, Lukas Bulwahn, Florian Haftmann. tphol 2009: 131-146 [doi]

Formalizing the Logic-Automaton ConnectionStefan Berghofer, Markus Reiter. tphol 2009: 147-163 [doi]

Formalizing the Logic-Automaton ConnectionStefan Berghofer, Markus Reiter. afp, 2009, 2009. [doi]

2008

Nominal Inversion PrinciplesStefan Berghofer, Christian Urban. tphol 2008: 71-85 [doi]

Logic-Free Reasoning in Isabelle/IsarStefan Berghofer, Makarius Wenzel. AISC 2008: 355-369 [doi]

Mechanizing the Metatheory of LFChristian Urban, James Cheney, Stefan Berghofer. lics 2008: 45-56 [doi]

2007

A Head-to-Head Comparison of de Bruijn Indices and NamesStefan Berghofer, Christian Urban. ENTCS, 174(5):53-67, 2007. [doi]

First-Order Logic According to FittingStefan Berghofer. afp, 2007, 2007. [doi]

POPLmark Challenge Via de Bruijn IndicesStefan Berghofer. afp, 2007, 2007. [doi]

Barendregt s Variable Convention in Rule InductionsChristian Urban, Stefan Berghofer, Michael Norrish. cade 2007: 35-50 [doi]

2006

Program Extraction from Normalization ProofsUlrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg. sLogica, 82(1):25-49, 2006. [doi]

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOLChristian Urban, Stefan Berghofer. cade 2006: 498-512 [doi]

2004

Extracting a Normalization Algorithm in Isabelle/HOLStefan Berghofer. TYPES 2006: 50-65 [doi]

Random Testing in Isabelle/HOLStefan Berghofer, Tobias Nipkow. SEFM 2004: 230-239 [doi]

2003

A Constructive Proof of Higman s Lemma in IsabelleStefan Berghofer. TYPES 2004: 66-82 [doi]

Extracting a formally verified, fully executable compiler from a proof assistantStefan Berghofer, Martin Strecker. ENTCS, 82(2):377-394, 2003. [doi]

Proofs, programs and executable specifications in higher order logicStefan Berghofer. PhD thesis, Technical University Munich, 2003. [doi]

2002

Program Extraction in Simply-Typed Higher Order LogicStefan Berghofer. TYPES 2003: 21-38 [doi]

2001

Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of ContextsChristine Röckl, Daniel Hirschkoff, Stefan Berghofer. fossacs 2001: 364-378 [doi]

2000

Proof Terms for Simply Typed Higher Order LogicStefan Berghofer, Tobias Nipkow. tphol 2000: 38-52

Executing Higher Order LogicStefan Berghofer, Tobias Nipkow. TYPES 2002: 24-40 [doi]

1999

Inductive Datatypes in HOL - Lessons Learned in Formal-Logic EngineeringStefan Berghofer, Markus Wenzel. tphol 1999: 19-36 [doi]

Sign in or sign up to see more results.

runs on WebDSL