| 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 | 463 | 2009 |
| Internal type theory P Dybjer International Workshop on Types for Proofs and Programs, 120-134, 1995 | 426 | 1995 |
| Inductive families P Dybjer Formal aspects of computing 6 (4), 440-465, 1994 | 327 | 1994 |
| A general formulation of simultaneous inductive-recursive definitions in type theory P Dybjer The journal of symbolic logic 65 (2), 525-549, 2000 | 268 | 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 | 208 | 1990 |
| A finite axiomatization of inductive-recursive definitions P Dybjer, A Setzer International Conference on Typed Lambda Calculi and Applications, 129-146, 1999 | 155 | 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 | 144 | 2001 |
| Dependent types at work A Bove, P Dybjer International LerNet ALFA Summer School on Language Engineering and Rigorous …, 2008 | 136 | 2008 |
| 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 | 123 | 2014 |
| Universes for generic programs and proofs in dependent type theory M Benke, P Dybjer, P Jansson Nord. J. Comput. 10 (4), 265-289, 2003 | 118 | 2003 |
| Intuitionistic model constructions and normalization proofs T Coquand, P Dybjer Mathematical Structures in Computer Science 7 (1), 75-94, 1997 | 117 | 1997 |
| Induction–recursion and initial algebras P Dybjer, A Setzer Annals of Pure and Applied Logic 124 (1-3), 1-47, 2003 | 103 | 2003 |
| Representing inductively defined sets by wellorderings in Martin-Löf's type theory P Dybjer Theoretical computer science 176 (1-2), 329-335, 1997 | 73 | 1997 |
| Indexed induction–recursion P Dybjer, A Setzer The Journal of Logic and Algebraic Programming 66 (1), 1-49, 2006 | 72 | 2006 |
| Normalization and partial evaluation P Dybjer, A Filinski International Summer School on Applied Semantics, 137-192, 2000 | 72 | 2000 |
| 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 | 69 | 2007 |
| 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 | 69 | 2003 |
| Normalization and the Yoneda embedding D Čubrić, P Dybjer, P Scott Mathematical Structures in Computer Science 8 (2), 153-192, 1998 | 69 | 1998 |
| Indexed induction-recursion P Dybjer, A Setzer International Seminar on Proof Theory in Computer Science, 93-113, 2001 | 53 | 2001 |
| Categories with families: Unityped, simply typed, and dependently typed S Castellan, P Clairambault, P Dybjer Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, 135-180, 2021 | 52 | 2021 |
Anton SetzerDept of Computerv Science, Swansea UniversityVerified email at swansea.ac.uk
