Stefan Berghofer

According to our database1, Stefan Berghofer authored at least 25 papers between 1999 and 2017.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2017
The Group Law for Elliptic Curves.
Arch. Formal Proofs, 2017

2012
A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL.
J. Autom. Reason., 2012

2011
Mechanizing the metatheory of LF.
ACM Trans. Comput. Log., 2011

Verification of Dependable Software using SPARK and Isabelle.
Proceedings of the 6th International Workshop on Systems Software Verification, 2011

Extending Hindley-Milner Type Inference with Coercive Structural Subtyping.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2009
Formalizing the Logic-Automaton Connection.
Arch. Formal Proofs, 2009

Turning Inductive into Equational Specifications.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2008
Nominal Inversion Principles.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Logic-Free Reasoning in Isabelle/Isar.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007
POPLmark Challenge Via de Bruijn Indices.
Arch. Formal Proofs, 2007

First-Order Logic According to Fitting.
Arch. Formal Proofs, 2007

Barendregt's Variable Convention in Rule Inductions.
Proceedings of the Automated Deduction, 2007

2006
Program Extraction from Normalization Proofs.
Stud Logica, 2006

A Head-to-Head Comparison of de Bruijn Indices and Names.
Proceedings of the First International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2006

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2004
Extracting a Normalization Algorithm in Isabelle/HOL.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Random Testing in Isabelle/HOL.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

2003
Proofs, programs and executable specifications in higher order logic.
PhD thesis, 2003

Extracting a formally verified, fully executable compiler from a proof assistant.
Proceedings of the Compiler Optimization Meets Compiler Verification, 2003

A Constructive Proof of Higman's Lemma in Isabelle.
Proceedings of the Types for Proofs and Programs, International Workshop, 2003

2002
Program Extraction in Simply-Typed Higher Order Logic.
Proceedings of the Types for Proofs and Programs, Second International Workshop, 2002

2001
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts.
Proceedings of the Foundations of Software Science and Computation Structures, 2001

2000
Executing Higher Order Logic.
Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Proof Terms for Simply Typed Higher Order Logic.
Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1999
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.
Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999


  Loading...