Please note: This is a beta version of the new dblp website.
You can find the classic dblp view of this page here.

Stefan Berghofer

2010 – today

see FAQ

What is the meaning of the colors in the publication list?

2012
[j8]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/jar/Berghofer12
- ask others
Stefan Berghofer: A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL. J. Autom. Reasoning 49(3): 303-326 (2012)
2011
[j7]
- view
  - electronic edition @ acm.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/tocl/UrbanCB11
- ask others
Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2): 15 (2011)
[c17]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/aplas/TraytelBN11
- ask others
Dmitriy Traytel, Stefan Berghofer, Tobias Nipkow: Extending Hindley-Milner Type Inference with Coercive Structural Subtyping. APLAS 2011: 89-104
[c16]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/ssv/Berghofer11
- ask others
Stefan Berghofer: Verification of Dependable Software using SPARK and Isabelle. SSV 2011: 15-31

2000 – 2009

see FAQ

What is the meaning of the colors in the publication list?

2009
[j6]
- view
  - electronic edition @ sourceforge.net
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/afp/BerghoferR09
- ask others
Stefan Berghofer, Markus Reiter: Formalizing the Logic-Automaton Connection. Archive of Formal Proofs 2009 (2009)
[c15]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/BerghoferBH09
- ask others
Stefan Berghofer, Lukas Bulwahn, Florian Haftmann: Turning Inductive into Equational Specifications. TPHOLs 2009: 131-146
[c14]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/BerghoferR09
- ask others
Stefan Berghofer, Markus Reiter: Formalizing the Logic-Automaton Connection. TPHOLs 2009: 147-163
[e1]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/2009
- ask others
Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (Eds.): Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, ISBN 978-3-642-03358-2
2008
[c13]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/aisc/BerghoferW08
- ask others
Stefan Berghofer, Makarius Wenzel: Logic-Free Reasoning in Isabelle/Isar. AISC/MKM/Calculemus 2008: 355-369
[c12]
- view
  - electronic edition @ ieeecomputersociety.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/lics/UrbanCB08
- ask others
Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF. LICS 2008: 45-56
[c11]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/BerghoferU08
- ask others
Stefan Berghofer, Christian Urban: Nominal Inversion Principles. TPHOLs 2008: 71-85
[i1]
- view
  - electronic edition @ arxiv.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/corr/abs-0804-1667
- ask others
Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF. CoRR abs/0804.1667 (2008)
2007
[j5]
- view
  - electronic edition @ sourceforge.net
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/afp/Berghofer07
- ask others
Stefan Berghofer: First-Order Logic According to Fitting. Archive of Formal Proofs 2007 (2007)
[j4]
- view
  - electronic edition @ sourceforge.net
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/afp/Berghofer07a
- ask others
Stefan Berghofer: POPLmark Challenge Via de Bruijn Indices. Archive of Formal Proofs 2007 (2007)
[j3]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/entcs/BerghoferU07
- ask others
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)
[c10]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/cade/UrbanBN07
- ask others
Christian Urban, Stefan Berghofer, Michael Norrish: Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50
2006
[j2]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/sLogica/BergerBLS06
- ask others
Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg: Program Extraction from Normalization Proofs. Studia Logica 82(1): 25-49 (2006)
[c9]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/cade/UrbanB06
- ask others
Christian Urban, Stefan Berghofer: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR 2006: 498-512
2004
[c8]
- view
  - electronic edition @ ieeecomputersociety.org
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/sefm/BerghoferN04
- ask others
Stefan Berghofer, Tobias Nipkow: Random Testing in Isabelle/HOL. SEFM 2004: 230-239
[c7]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/types/Berghofer04
- ask others
Stefan Berghofer: Extracting a Normalization Algorithm in Isabelle/HOL. TYPES 2004: 50-65
2003
[b1]
- view
  - electronic edition @ tu-muenchen.de
- export record as
  - BibTeX
  - XML
  dblp key:
  - phd/de/Berghofer2003
- ask others
Stefan Berghofer: Proofs, programs and executable specifications in higher order logic. Technical University Munich 2003, pp. 1-161
[j1]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - journals/entcs/BerghoferS03
- ask others
Stefan Berghofer, Martin Strecker: Extracting a formally verified, fully executable compiler from a proof assistant. Electr. Notes Theor. Comput. Sci. 82(2): 377-394 (2003)
[c6]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/types/Berghofer03
- ask others
Stefan Berghofer: A Constructive Proof of Higman's Lemma in Isabelle. TYPES 2003: 66-82
2002
[c5]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/types/Berghofer02
- ask others
Stefan Berghofer: Program Extraction in Simply-Typed Higher Order Logic. TYPES 2002: 21-38
2001
[c4]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/fossacs/RocklHB01
- ask others
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
[c3]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/BerghoferN00
- ask others
Stefan Berghofer, Tobias Nipkow: Proof Terms for Simply Typed Higher Order Logic. TPHOLs 2000: 38-52
[c2]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/types/BerghoferN00
- ask others
Stefan Berghofer, Tobias Nipkow: Executing Higher Order Logic. TYPES 2000: 24-40

1990 – 1999

see FAQ

What is the meaning of the colors in the publication list?

1999
[c1]
- view
  - electronic edition via DOI
- export record as
  - BibTeX
  - XML
  dblp key:
  - conf/tphol/BerghoferW99
- ask others
Stefan Berghofer, Markus Wenzel: Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. TPHOLs 1999: 19-36