Travelled to:1 × China
1 × Germany
1 × Italy
2 × USA
Collaborated with:C.Urban T.Nipkow J.Cheney M.Norrish C.Röckl D.Hirschkoff
Talks about:isabell (3) hol (3) mechan (2) induct (2) metatheori (1) barendregt (1) implement (1) calculus (1) abstract (1) variabl (1)
Person: Stefan Berghofer
DBLP: Berghofer:Stefan
Contributed to:
2008
2007
2006
2004
2001Wrote 5 papers:
- LICS-2008-UrbanCB
- Mechanizing the Metatheory of LF (CU, JC, SB), pp. 45–56.
- CADE-2007-UrbanBN
- Barendregt’s Variable Convention in Rule Inductions (CU, SB, MN), pp. 35–50.
- IJCAR-2006-UrbanB #combinator #data type #higher-order #recursion
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
- SEFM-2004-BerghoferN #higher-order #random testing #testing
- Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
- FoSSaCS-2001-RocklHB #formal method #higher-order #induction #syntax #π-calculus
- Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts (CR, DH, SB), pp. 364–378.