Bove, Ana; Dybjer, Peter; Andrés, Sicard-Ramírez: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012, 7213 pp. 104-118. ISBN/ISSN: 978-3-642-28728-2
Dybjer, Peter; Kuperberg, D.: Formal neighbourhoods, combinatory Bohm trees, and untyped normalization by evaluation. Annals of Pure and Applied Logic, 163 (2) pp. 122-131. 2011
Clairambault, P.; Dybjer, Peter: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. Lecture Notes in Computer Science. 10th International Conference on Typed Lambda Calculi and Applications, TLCA 2011, Novi Sad,1-3 June 2011, 6690 pp. 91-106. ISBN/ISSN: 978-364221690-9 2009
Bove, Ana; Dybjer, Peter; Norell, Ulf: A Brief Overview of Agda - A Functional Language with Dependent Types. Theorem Proving in Higher Order Logics , 5674 (LNCS) pp. 73--78.
Bove, Ana; Dybjer, Peter: Dependent Types at Work. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer Schoo, 5520 (LNCS) pp. 57--99.
Bove, Ana; Dybjer, Peter; Sicard-Ramirez, Andres: Embedding a Logical Theory of Constructions in Agda. Programming Languages meets Program Verification (PLPV) 2009 , (ACM digital library) 2008
Abel, Andreas; Coquand, Thierry; Dybjer, Peter: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008, pp. 3-13.
Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. Mathematics of Program Construction 2008, pp. 29-56.
Dybjer, Peter; Buisse, Alexandre: The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. Electr. Notes Theor. Comput. Sci., (218) pp. 21-32. 2007
Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements. Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.,
Abel, Andreas; Aehlig, Klaus; Dybjer, Peter: Normalization by evaluation for Martin-Löf type theory with one universe. Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Ed. M. Fiore. Electronic Notes in Theoretical Computer Science, Elsevier., 173 pp. 17-40.
Buisse, Alexandre; Dybjer, Peter: Towards formalizing categorical models of type theory in type theory. Second International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP'07), eds Brigite Pientka and Carsten Schurmann, Electronic Notes in Theoretical Computer Science, Elsevier , pp. 72-85. 2006
Dybjer, Peter; Setzer, Anton: Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66 (1) pp. 1-49. 2004
Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Random generators for dependent types. Proceedings of the First International Colloquium on Theoretical Aspects of Computing, Guiyang, China, September 2004, pp. 342 -356 .
Dybjer, Peter; Haiyan, Qiao; Takeyama, Makoto: Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information and Software Technology, special issue, edited by Huimin Lin, Hans-Dieter Ehrich, and T.H. Tse, 46 (15) pp. 1011 - 1025. 2003
Benke, Marcin; Dybjer, Peter; Jansson, Patrik: Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic Journal of Computing, 10 (4) pp. 265-289.
Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Combining testing and proving in dependent type theory. Lecture Notes in Computer Science. Proceedings - 16th International Conference on Theorem Proving in Higher Order Logics, Rome, 8-12 September 2003, 2758 pp. 188-203. ISBN/ISSN: 3-540-40664-6
Dybjer, Peter; Setzer, Anton: Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124 (1-3) pp. 1-47.
Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Verifying Haskell programs by combining testing and proving. Proceedings 3rd International Conference on Quality Software, IEEE Computer Society Press, pp. 272-279. ISBN/ISSN: 0-7695-2015-4 2002
Dybjer, Peter; Filinski, Andrzej: Normalization and Partial Evaluation. Lecture Notes in Computer Science. International Summer School, APPSEM 2000 Caminha, Portugal, September 9–15, 2000, 2395 pp. 137-192 . ISBN/ISSN: 978-3-540-44044-4 2001
Dybjer, Peter; Setzer, Anton: Indexed induction-recursion. Proof Theory in Computer Science · International Seminar, LNCS, 2183 pp. 93-113.
Dybjer, Peter; Altenkirch, Thorsten; Hofmann, Martin; Scott, Philip: Normalization by evaluation for typed lambda calculus with coproducts. Proceedings of 16th Annual Symposium on Logic in Computer Science, pp. 203-210. 2000
Dybjer, Peter: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65 (2) pp. 525-549. 1999
Dybjer, Peter; Setzer, Anton: A finite axiomatization of inductive-recursive definitions. Proceedings of TLCA 1999, LNCS, 1581 pp. 129 - 146. 1998
Dybjer, Peter; Cubric, Djordje; Scott, Philip: Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8 pp. 153-192. 1997
Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7 pp. 75-94.
Dybjer, Peter: Representing inductively defined sets by well-orderings in Martin-Löf's type theory. Theoretical Computer Science, 176 pp. 329-335. 1996
Dybjer, Peter; Beylin, Ilya; Agerholm, Sten: A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. Theorem Proving in Higher Order Logics, LNCS, 1125 pp. 17-32.
Dybjer, Peter; Beylin, Ilya: Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids. TYPES '95, LNCS, 1158 pp. 47-61.
Dybjer, Peter: Internal type theory. TYPES '95, LNCS, 1158 pp. 120-134. 1994
Dybjer, Peter: Inductive Families. Formal Aspects of Computing, 6 pp. 440-465.
Dybjer, Peter; Coquand, Thierry: Inductive definitions and type theory an introduction. Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India, LNCS, 880 1993
Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Proceedings of the 1993 TYPES Workshop, Nijmegen, 1991
Dybjer, Peter: Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics. Logical Frameworks, pp. 280-306.
Dybjer, Peter: Inverse image analysis generalises strictness analysis. Information and Computation, 90 (2) pp. 194--216. 1990
Dybjer, Peter: Comparing integrated and external logics of functional programs. Science of Computer Programming, 14 pp. 59--79. 1989
Dybjer, Peter; Sander, Herbert: A functional programming approach to the specification and verification of concurrent systems. Formal Aspects of Computing, 1 pp. 303-319.