Peter Dybjer
Peter Dybjer
Professor of Computer Science, Chalmers University
Verified email at - Homepage
Cited by
Cited by
A brief overview of Agda–a functional language with dependent types
A Bove, P Dybjer, U Norell
Theorem Proving in Higher Order Logics: 22nd International Conference …, 2009
Internal type theory
P Dybjer
International Workshop on Types for Proofs and Programs, 120-134, 1995
Inductive families
P Dybjer
Formal aspects of computing 6, 440-465, 1994
A general formulation of simultaneous inductive-recursive definitions in type theory
P Dybjer
The journal of symbolic logic 65 (2), 525-549, 2000
Inductive sets and families in Martin-L of's type theory and their set-theoretic semantics
P Dybjer
Informal Proceedings of the First Workshop on Logical Frameworks, 213-230, 1990
A finite axiomatization of inductive-recursive definitions
P Dybjer, A Setzer
Typed Lambda Calculi and Applications: 4th International Conference, TLCA’99 …, 1999
Normalization by evaluation for typed lambda calculus with coproducts
T Altenkirch, P Dybjer, M Hofmann, P Scott
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, 303-310, 2001
Dependent types at work
A Bove, P Dybjer
International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008
Intuitionistic model constructions and normalization proofs
T Coquand, P Dybjer
Mathematical Structures in Computer Science 7 (1), 75-94, 1997
Universes for generic programs and proofs in dependent type theory
M Benke, P Dybjer, P Jansson
Nord. J. Comput. 10 (4), 265-289, 2003
Induction–recursion and initial algebras
P Dybjer, A Setzer
Annals of Pure and Applied Logic 124 (1-3), 1-47, 2003
The biequivalence of locally cartesian closed categories and Martin-Löf type theories
P Clairambault, P Dybjer
Mathematical Structures in Computer Science 24 (6), e240606, 2014
Normalization and partial evaluation
P Dybjer, A Filinski
International Summer School on Applied Semantics, 137-192, 2000
Representing inductively defined sets by wellorderings in Martin-Löf's type theory
P Dybjer
Theoretical computer science 176 (1-2), 329-335, 1997
Indexed induction–recursion
P Dybjer, A Setzer
The Journal of Logic and Algebraic Programming 66 (1), 1-49, 2006
Combining testing and proving in dependent type theory
P Dybjer, Q Haiyan, M Takeyama
Theorem Proving in Higher Order Logics: 16th International Conference …, 2003
Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements
A Abel, T Coquand, P Dybjer
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 3-12, 2007
Normalization and the Yoneda embedding
D Čubrić, P Dybjer, P Scott
Mathematical Structures in Computer Science 8 (2), 153-192, 1998
Indexed induction-recursion
P Dybjer, A Setzer
Proof Theory in Computer Science: International Seminar, PTCS 2001 Dagstuhl …, 2001
Normalization by evaluation for Martin-Löf type theory with one universe
A Abel, K Aehlig, P Dybjer
Electronic Notes in Theoretical Computer Science 173, 17-39, 2007
The system can't perform the operation now. Try again later.
Articles 1–20