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.

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

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)

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.

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.

Dybjer, Peter; Setzer, Anton: Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66 (1) pp. 1-49.

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.

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

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

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.

Dybjer, Peter: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65 (2) pp. 525-549.

Dybjer, Peter; Setzer, Anton: A finite axiomatization of inductive-recursive definitions. Proceedings of TLCA 1999, LNCS, 1581 pp. 129 - 146.

Dybjer, Peter; Cubric, Djordje; Scott, Philip: Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8 pp. 153-192.

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.

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.

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

Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Proceedings of the 1993 TYPES Workshop, Nijmegen,

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.

Dybjer, Peter: Comparing integrated and external logics of functional programs. Science of Computer Programming, 14 pp. 59--79.

Dybjer, Peter; Sander, Herbert: A functional programming approach to the specification and verification of concurrent systems. Formal Aspects of Computing, 1 pp. 303-319.