Travelled to:
1 × Belgium
1 × Estonia
1 × France
1 × Germany
1 × Italy
1 × Japan
1 × Serbia
1 × USA
1 × United Kingdom
2 × Poland
Collaborated with:
∅ P.Clairambault A.Abel T.Coquand A.Setzer S.Castellan A.Bove A.Sicard-Ramírez T.Altenkirch M.Hofmann P.J.Scott
Talks about:
theori (5) type (5) normal (3) evalu (3) cartesian (2) categori (2) program (2) algebra (2) martin (2) local (2)
Person: Peter Dybjer
DBLP: Dybjer:Peter
Contributed to:
Wrote 11 papers:
- FoSSaCS-2015-ClairambaultD #evaluation #game studies #normalisation #semantics
- Game Semantics and Normalization by Evaluation (PC, PD), pp. 56–70.
- TLCA-2015-CastellanCD #similarity
- Undecidability of Equality in the Free Locally Cartesian Closed Category (SC, PC, PD), pp. 138–152.
- FoSSaCS-2012-BoveDS #automation #first-order #functional #interactive #reasoning #source code
- Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs (AB, PD, ASR), pp. 104–118.
- TLCA-2011-ClairambaultD #category theory
- The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (PC, PD), pp. 91–106.
- FLOPS-2008-AbelCD #algebra #on the #proving #type system
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
- LICS-2007-AbelCD #evaluation #normalisation #similarity #type system
- Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (AA, TC, PD), pp. 3–12.
- LICS-2001-AltenkirchDHS #evaluation #normalisation #λ-calculus
- Normalization by Evaluation for Typed λ Calculus with Coproducts (TA, PD, MH, PJS), pp. 303–310.
- TLCA-1999-DybjerS #axiom #finite #recursion
- A Finite Axiomatization of Inductive-Recursive Definitions (PD, AS), pp. 129–146.
- ICALP-1987-Dybjer #analysis #image
- Inverse Image Analysis (PD), pp. 21–30.
- FPCA-1985-Dybjer85 #logic #verification
- Program Verification in a Logical Theory of Constructions (PD), pp. 334–349.
- ICALP-1984-Dybjer #algebra
- Domain Algebras (PD), pp. 138–150.