BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Dybjer:Peter

Contributed to:

FoSSaCS 20152015
TLCA 20152015
FOSSACS 20122012
TLCA 20112011
FLOPS 20082008
LICS 20072007
LICS 20012001
TLCA 19991999
ICALP 19871987
FPCA 19851985
ICALP 19841984

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.