Towards a Unified Theory of Data Types: Some Categorical Aspects. - Peter Dybjer (ADT, 1983)

Domain Algebras. - Peter Dybjer (ICALP, 1984)

Some Results on the Deductive Structure of Join Dependencies. - Peter Dybjer (Theor. Comput. Sci., 1984)

Category Theory and Programming Language Semantics: an Overview. - Peter Dybjer (CTCS, 1985)

Program Verification in a Logical Theory of Constructions. - Peter Dybjer (FPCA, 1985)

Using Domain Algebras to Prove the Correctness of a Compiler. - Peter Dybjer (STACS, 1985)

Inverse Image Analysis. - Peter Dybjer (ICALP, 1987)

A Functional Programming Approach to the Specification and Verification of Concurrent Systems. - Peter Dybjer; Herbert P. Sander (Formal Aspects Comput., 1989)

Comparing Integrated and External Logics of Functional Programs. - Peter Dybjer (Sci. Comput. Program., 1990)

Inverse Image Analysis Generalises Strictness Analysis - Peter Dybjer (Inf. Comput., 1991)

Inductive Definitions and Type Theory: an Introduction (Preliminary Version). - Thierry Coquand; Peter Dybjer (FSTTCS, 1994)

Inductive Families. - Peter Dybjer (Formal Aspects Comput., 1994)

Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. - Ilya Beylin; Peter Dybjer (TYPES, 1995)

Internal Type Theory. - Peter Dybjer (TYPES, 1995)

A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. - Sten Agerholm; Ilya Beylin; Peter Dybjer (TPHOLs, 1996)

Intuitionistic Model Constructions and Normalization Proofs. - Thierry Coquand; Peter Dybjer (Math. Struct. Comput. Sci., 1997)

Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. - Peter Dybjer (Theor. Comput. Sci., 1997)

Normalization and the Yoneda Embedding. - Djordje Cubric; Peter Dybjer; Philip J. Scott (Math. Struct. Comput. Sci., 1998)

A Finite Axiomatization of Inductive-Recursive Definitions. - Peter Dybjer; Anton Setzer (TLCA, 1999)

Normalization and Partial Evaluation. - Peter Dybjer; Andrzej Filinski (APPSEM, 2000)

A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. - Peter Dybjer (J. Symb. Log., 2000)

Normalization by Evaluation for Typed Lambda Calculus with Coproducts. - Thorsten Altenkirch; Peter Dybjer; Martin Hofmann 001; Philip J. Scott (LICS, 2001)

Verifying Haskell Programs by Combining Testing and Proving. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (QSIC, 2003)

Combining Testing and Proving in Dependent Type Theory. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (TPHOLs, 2003)

Induction-recursion and initial algebras. - Peter Dybjer; Anton Setzer (Ann. Pure Appl. Log., 2003)

Universes for Generic Programs and Proofs in Dependent Type Theory. - Marcin Benke; Peter Dybjer; Patrik Jansson (Nord. J. Comput., 2003)

Random Generators for Dependent Types. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (ICTAC, 2004)

Verifying Haskell programs by combining testing, model checking and interactive theorem proving. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (Inf. Softw. Technol., 2004)

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. - Gilles Barthe; Peter Dybjer; Peter Thiemann 001 (J. Funct. Program., 2004)

Indexed induction-recursion. - Peter Dybjer; Anton Setzer (J. Log. Algebraic Methods Program., 2006)

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (LICS, 2007)

Normalization by Evaluation for Martin-Löf Type Theory with One Universe. - Andreas Abel 001; Klaus Aehlig; Peter Dybjer (MFPS, 2007)

Towards Formalizing Categorical Models of Type Theory in Type Theory. - Alexandre Buisse; Peter Dybjer (LFMTP@CADE, 2007)

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (FLOPS, 2008)

Dependent Types at Work. - Ana Bove; Peter Dybjer (LerNet ALFA Summer School, 2008)

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. - Andreas Abel 001; Thierry Coquand; Peter Dybjer (MPC, 2008)

The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. - Alexandre Buisse; Peter Dybjer (MFPS, 2008)

Embedding a logical theory of constructions in Agda. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (PLPV, 2009)

A Brief Overview of Agda - A Functional Language with Dependent Types. - Ana Bove; Peter Dybjer; Ulf Norell (TPHOLs, 2009)

Agda Implementors Meeting (NII Shonan Meeting 2011-2). - Peter Dybjer; Yoshiki Kinoshita; Shin-Cheng Mu (NII Shonan Meet. Rep., 2011)

Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (FoSSaCS, 2012)

Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. - Peter Dybjer; Denis Kuperberg (Ann. Pure Appl. Log., 2012)

Program Testing and the Meaning Explanations of Intuitionistic Type Theory. - Peter Dybjer (Epistemology versus Ontology, 2012)

The biequivalence of locally cartesian closed categories and Martin-Löf type theories. - Pierre Clairambault; Peter Dybjer (Math. Struct. Comput. Sci., 2014)

Game Semantics and Normalization by Evaluation. - Pierre Clairambault; Peter Dybjer (FoSSaCS, 2015)

Undecidability of Equality in the Free Locally Cartesian Closed Category. - Simon Castellan; Pierre Clairambault; Peter Dybjer (TLCA, 2015)

Special issue on Programming with Dependent Types Editorial. - Wouter Swierstra; Peter Dybjer (J. Funct. Program., 2017)

Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). - Simon Castellan; Pierre Clairambault; Peter Dybjer (Log. Methods Comput. Sci., 2017)

Finitary Higher Inductive Types in the Groupoid Model. - Peter Dybjer; Hugo Moeneclaey (MFPS, 2018)

Categories with Families: Unityped, Simply Typed, and Dependently Typed. - Simon Castellan; Pierre Clairambault; Peter Dybjer (CoRR, 2019)

A Note on Generalized Algebraic Theories and Categories with Families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2020)

On generalized algebraic theories and categories with families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (Math. Struct. Comput. Sci., 2021)

Type Theory with Explicit Universe Polymorphism. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (TYPES, 2022)

Type Theories with Universe Level Judgements. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2022)

The extended predicative Mahlo universe in Martin-Löf type theory. - Peter Dybjer; Anton Setzer (J. Log. Comput., 2024)