Peter Dybjer
Peter Dybjer
Professor of Computer Science, Chalmers University
Verified email at chalmers.se - Homepage
Title
Cited by
Cited by
Year
A brief overview of Agda–a functional language with dependent types
A Bove, P Dybjer, U Norell
International Conference on Theorem Proving in Higher Order Logics, 73-78, 2009
2912009
Inductive families
P Dybjer
Formal aspects of computing 6 (4), 440-465, 1994
2511994
Internal type theory
P Dybjer
International Workshop on Types for Proofs and Programs, 120-134, 1995
2481995
A general formulation of simultaneous inductive-recursive definitions in type theory
P Dybjer
Journal of Symbolic Logic, 525-549, 2000
2152000
type theory and their set-theoretic
P Dybjer
Logical frameworks 1, 280, 1991
1861991
A finite axiomatization of inductive-recursive definitions
P Dybjer, A Setzer
International Conference on Typed Lambda Calculi and Applications, 129-146, 1999
1221999
Dependent types at work
A Bove, P Dybjer
International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008
1002008
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
992001
Intuitionistic model constructions and normalization proofs
T Coquand, P Dybjer
Mathematical Structures in Computer Science 7 (1), 75-94, 1997
991997
Universes for generic programs and proofs in dependent type theory
M Benke, P Dybjer, P Jansson
Nord. J. Comput. 10 (4), 265-289, 2003
912003
Induction–recursion and initial algebras
P Dybjer, A Setzer
Annals of Pure and Applied Logic 124 (1-3), 1-47, 2003
732003
Normalization and partial evaluation
P Dybjer, A Filinski
International Summer School on Applied Semantics, 137-192, 2000
602000
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
582007
Combining testing and proving in dependent type theory
P Dybjer, Q Haiyan, M Takeyama
International Conference on Theorem Proving in Higher Order Logics, 188-203, 2003
552003
The biequivalence of locally cartesian closed categories and Martin-Löf type theories
P Clairambault, P Dybjer
542014
Normalization and the Yoneda embedding
D Cubric, P Dybjer, P Scott
Mathematical Structures in Computer Science 8 (2), 153-192, 1998
541998
Indexed induction–recursion
P Dybjer, A Setzer
The Journal of Logic and Algebraic Programming 66 (1), 1-49, 2006
522006
Representing inductively defined sets by wellorderings in Martin-Löf's type theory
P Dybjer
Theoretical Computer Science 176 (1-2), 329-335, 1997
521997
Indexed induction-recursion
P Dybjer, A Setzer
International Seminar on Proof Theory in Computer Science, 93-113, 2001
482001
A functional programming approach to the specification and verification of concurrent systems
P Dybjer, HP Sander
Formal Aspects of Computing 1 (1), 303-319, 1989
431989
The system can't perform the operation now. Try again later.
Articles 1–20