Peter Dybjer
Peter Dybjer
Professor of Computer Science, Chalmers University
Bestätigte E-Mail-Adresse bei chalmers.se - Startseite
Titel
Zitiert von
Zitiert von
Jahr
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
2942009
Internal type theory
P Dybjer
International Workshop on Types for Proofs and Programs, 120-134, 1995
2621995
Inductive families
P Dybjer
Formal aspects of computing 6 (4), 440-465, 1994
2541994
A general formulation of simultaneous inductive-recursive definitions in type theory
P Dybjer
Journal of Symbolic Logic, 525-549, 2000
2212000
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
1891990
A finite axiomatization of inductive-recursive definitions
P Dybjer, A Setzer
International Conference on Typed Lambda Calculi and Applications, 129-146, 1999
1221999
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
1032001
Dependent types at work
A Bove, P Dybjer
International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008
1022008
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
892003
Induction–recursion and initial algebras
P Dybjer, A Setzer
Annals of Pure and Applied Logic 124 (1-3), 1-47, 2003
762003
Normalization and partial evaluation
P Dybjer, A Filinski
International Summer School on Applied Semantics, 137-192, 2000
622000
The biequivalence of locally cartesian closed categories and Martin-Löf type theories
P Clairambault, P Dybjer
Mathematical Structures in Computer Science 24 (05), e240501, 2014
572014
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
562007
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
562003
Indexed induction–recursion
P Dybjer, A Setzer
The Journal of Logic and Algebraic Programming 66 (1), 1-49, 2006
542006
Representing inductively defined sets by wellorderings in Martin-Löf's type theory
P Dybjer
Theoretical Computer Science 176 (1-2), 329-335, 1997
541997
Normalization and the Yoneda embedding
D Cubric, P Dybjer, P Scott
Mathematical Structures in Computer Science 8 (2), 153-192, 1998
531998
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
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20