The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Stefan Berghofer: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Christian Urban, Stefan Berghofer
    A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2006, pp:498-512 [Conf]
  2. 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. [Citation Graph (0, 0)][DBLP]
    FoSSaCS, 2001, pp:364-378 [Conf]
  3. Stefan Berghofer, Tobias Nipkow
    Random Testing in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    SEFM, 2004, pp:230-239 [Conf]
  4. Stefan Berghofer, Tobias Nipkow
    Proof Terms for Simply Typed Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:38-52 [Conf]
  5. Stefan Berghofer, Markus Wenzel
    Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 1999, pp:19-36 [Conf]
  6. Stefan Berghofer
    Program Extraction in Simply-Typed Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TYPES, 2002, pp:21-38 [Conf]
  7. Stefan Berghofer
    A Constructive Proof of Higman's Lemma in Isabelle. [Citation Graph (0, 0)][DBLP]
    TYPES, 2003, pp:66-82 [Conf]
  8. Stefan Berghofer
    Extracting a Normalization Algorithm in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TYPES, 2004, pp:50-65 [Conf]
  9. Stefan Berghofer, Tobias Nipkow
    Executing Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TYPES, 2000, pp:24-40 [Conf]
  10. Stefan Berghofer, Martin Strecker
    Extracting a formally verified, fully executable compiler from a proof assistant. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2003, v:82, n:2, pp:- [Journal]
  11. Stefan Berghofer, Christian Urban
    A Head-to-Head Comparison of de Bruijn Indices and Names. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2007, v:174, n:5, pp:53-67 [Journal]
  12. Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg
    Program Extraction from Normalization Proofs. [Citation Graph (0, 0)][DBLP]
    Studia Logica, 2006, v:82, n:1, pp:25-49 [Journal]
  13. Christian Urban, Stefan Berghofer, Michael Norrish
    Barendregt's Variable Convention in Rule Inductions. [Citation Graph (0, 0)][DBLP]
    CADE, 2007, pp:35-50 [Conf]

  14. Logic-Free Reasoning in Isabelle/Isar. [Citation Graph (, )][DBLP]


  15. Mechanizing the Metatheory of LF. [Citation Graph (, )][DBLP]


  16. Nominal Inversion Principles. [Citation Graph (, )][DBLP]


  17. Formalizing the Logic-Automaton Connection. [Citation Graph (, )][DBLP]


  18. Turning Inductive into Equational Specifications. [Citation Graph (, )][DBLP]


  19. Mechanizing the Metatheory of LF [Citation Graph (, )][DBLP]


Search in 0.002secs, Finished in 0.003secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002