| 2008 |
|---|
| 17 | EE | Stefan Berghofer,
Makarius Wenzel:
Logic-Free Reasoning in Isabelle/Isar.
AISC/MKM/Calculemus 2008: 355-369 |
| 16 | EE | Christian Urban,
James Cheney,
Stefan Berghofer:
Mechanizing the Metatheory of LF.
LICS 2008: 45-56 |
| 15 | EE | Stefan Berghofer,
Christian Urban:
Nominal Inversion Principles.
TPHOLs 2008: 71-85 |
| 14 | EE | Christian Urban,
James Cheney,
Stefan Berghofer:
Mechanizing the Metatheory of LF
CoRR abs/0804.1667: (2008) |
| 2007 |
|---|
| 13 | EE | Christian Urban,
Stefan Berghofer,
Michael Norrish:
Barendregt's Variable Convention in Rule Inductions.
CADE 2007: 35-50 |
| 12 | EE | Stefan Berghofer,
Christian Urban:
A Head-to-Head Comparison of de Bruijn Indices and Names.
Electr. Notes Theor. Comput. Sci. 174(5): 53-67 (2007) |
| 2006 |
|---|
| 11 | EE | Christian Urban,
Stefan Berghofer:
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
IJCAR 2006: 498-512 |
| 10 | EE | Ulrich Berger,
Stefan Berghofer,
Pierre Letouzey,
Helmut Schwichtenberg:
Program Extraction from Normalization Proofs.
Studia Logica 82(1): 25-49 (2006) |
| 2004 |
|---|
| 9 | EE | Stefan Berghofer,
Tobias Nipkow:
Random Testing in Isabelle/HOL.
SEFM 2004: 230-239 |
| 8 | EE | Stefan Berghofer:
Extracting a Normalization Algorithm in Isabelle/HOL.
TYPES 2004: 50-65 |
| 2003 |
|---|
| 7 | EE | Stefan Berghofer:
A Constructive Proof of Higman's Lemma in Isabelle.
TYPES 2003: 66-82 |
| 6 | EE | Stefan Berghofer,
Martin Strecker:
Extracting a formally verified, fully executable compiler from a proof assistant.
Electr. Notes Theor. Comput. Sci. 82(2): (2003) |
| 2002 |
|---|
| 5 | EE | Stefan Berghofer:
Program Extraction in Simply-Typed Higher Order Logic.
TYPES 2002: 21-38 |
| 2001 |
|---|
| 4 | EE | 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: 364-378 |
| 2000 |
|---|
| 3 | | Stefan Berghofer,
Tobias Nipkow:
Proof Terms for Simply Typed Higher Order Logic.
TPHOLs 2000: 38-52 |
| 2 | EE | Stefan Berghofer,
Tobias Nipkow:
Executing Higher Order Logic.
TYPES 2000: 24-40 |
| 1999 |
|---|
| 1 | EE | Stefan Berghofer,
Markus Wenzel:
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.
TPHOLs 1999: 19-36 |
