The SCEAS System
| |||||||

## Search the dblp DataBase
Stefan Berghofer:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
## Publications of Author- 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] - 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] - Stefan Berghofer, Tobias Nipkow
**Random Testing in Isabelle/HOL.**[Citation Graph (0, 0)][DBLP] SEFM, 2004, pp:230-239 [Conf] - Stefan Berghofer, Tobias Nipkow
**Proof Terms for Simply Typed Higher Order Logic.**[Citation Graph (0, 0)][DBLP] TPHOLs, 2000, pp:38-52 [Conf] - 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] - Stefan Berghofer
**Program Extraction in Simply-Typed Higher Order Logic.**[Citation Graph (0, 0)][DBLP] TYPES, 2002, pp:21-38 [Conf] - Stefan Berghofer
**A Constructive Proof of Higman's Lemma in Isabelle.**[Citation Graph (0, 0)][DBLP] TYPES, 2003, pp:66-82 [Conf] - Stefan Berghofer
**Extracting a Normalization Algorithm in Isabelle/HOL.**[Citation Graph (0, 0)][DBLP] TYPES, 2004, pp:50-65 [Conf] - Stefan Berghofer, Tobias Nipkow
**Executing Higher Order Logic.**[Citation Graph (0, 0)][DBLP] TYPES, 2000, pp:24-40 [Conf] - 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] - 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] - 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] - Christian Urban, Stefan Berghofer, Michael Norrish
**Barendregt's Variable Convention in Rule Inductions.**[Citation Graph (0, 0)][DBLP] CADE, 2007, pp:35-50 [Conf] **Logic-Free Reasoning in Isabelle/Isar.**[Citation Graph (, )][DBLP]**Mechanizing the Metatheory of LF.**[Citation Graph (, )][DBLP]**Nominal Inversion Principles.**[Citation Graph (, )][DBLP]**Formalizing the Logic-Automaton Connection.**[Citation Graph (, )][DBLP]**Turning Inductive into Equational Specifications.**[Citation Graph (, )][DBLP]**Mechanizing the Metatheory of LF**[Citation Graph (, )][DBLP]
Search in 0.002secs, Finished in 0.003secs | |||||||

| |||||||

| |||||||

System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002 for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002 |