Stefan Berghofer

Available identifiers

zbMath Open berghofer.stefanMaRDI QIDQ817699

List of research outcomes

Publication	Date of Publication	Type
Mechanizing the metatheory of LF	2015-09-17	Paper
A head-to-head comparison of de Bruijn indices and names	2014-01-10	Paper
A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL	2013-04-17	Paper
Formalizing the Logic-Automaton Connection	2009-10-20	Paper
Turning Inductive into Equational Specifications	2009-10-20	Paper
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL	2009-03-12	Paper
Barendregt’s Variable Convention in Rule Inductions	2009-03-06	Paper
Logic-Free Reasoning in Isabelle/Isar	2009-01-27	Paper
Nominal Inversion Principles	2008-12-04	Paper
Types for Proofs and Programs	2006-11-13	Paper
Program extraction from normalization proofs	2006-03-17	Paper
Types for Proofs and Programs	2005-12-23	Paper
https://portal.mardi4nfdi.de/entity/Q4736387	2004-08-09	Paper
https://portal.mardi4nfdi.de/entity/Q4435458	2003-11-12	Paper
https://portal.mardi4nfdi.de/entity/Q2769442	2002-02-05	Paper
https://portal.mardi4nfdi.de/entity/Q2754030	2001-11-11	Paper
https://portal.mardi4nfdi.de/entity/Q4945200	2000-10-26	Paper

Research outcomes over time

This page was built for person: Stefan Berghofer