Peter Dybjer

Publication Activity (10 Years)

Years Active: 1983-2022
Publications (10 Years): 8

Top Topics

Top Venues

Math. Struct. Comput. Sci.

J. Funct. Program.

Publications

Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
Type Theories with Universe Level Judgements. CoRR (2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
Type Theory with Explicit Universe Polymorphism. TYPES (2022)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. 31 (9) (2021)
Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
A Note on Generalized Algebraic Theories and Categories with Families. CoRR (2020)
Simon Castellan, Pierre Clairambault, Peter Dybjer
Categories with Families: Unityped, Simply Typed, and Dependently Typed. CoRR (2019)
Peter Dybjer, Hugo Moeneclaey
Finitary Higher Inductive Types in the Groupoid Model. MFPS (2018)
Wouter Swierstra, Peter Dybjer
Special issue on Programming with Dependent Types Editorial. J. Funct. Program. 27 (2017)
Simon Castellan, Pierre Clairambault, Peter Dybjer
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). Log. Methods Comput. Sci. 13 (4) (2017)
Pierre Clairambault, Peter Dybjer
Game Semantics and Normalization by Evaluation. FoSSaCS (2015)
Simon Castellan, Pierre Clairambault, Peter Dybjer
Undecidability of Equality in the Free Locally Cartesian Closed Category. CoRR (2015)
Simon Castellan, Pierre Clairambault, Peter Dybjer
Undecidability of Equality in the Free Locally Cartesian Closed Category. TLCA (2015)
Pierre Clairambault, Peter Dybjer
The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Math. Struct. Comput. Sci. 24 (6) (2014)
Peter Dybjer, Denis Kuperberg
Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Log. 163 (2) (2012)
Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez
Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. FoSSaCS (2012)
Pierre Clairambault, Peter Dybjer
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. TLCA (2011)
Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu
Agda Implementors Meeting (NII Shonan Meeting 2011-2). NII Shonan Meet. Rep. 2011 (2011)
Pierre Clairambault, Peter Dybjer
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories CoRR (2011)
Ana Bove, Peter Dybjer, Ulf Norell
A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs (2009)
Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez
Embedding a logical theory of constructions in Agda. PLPV (2009)
Alexandre Buisse, Peter Dybjer
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. MFPS (2008)
Alexandre Buisse, Peter Dybjer
Towards Formalizing Categorical Models of Type Theory in Type Theory. Electron. Notes Theor. Comput. Sci. 196 (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS (2008)
Ana Bove, Peter Dybjer
Dependent Types at Work. LerNet ALFA Summer School (2008)
Andreas Abel, Thierry Coquand, Peter Dybjer
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer
Normalization by Evaluation for Martin-Löf Type Theory with One Universe. MFPS (2007)
Peter Dybjer, Anton Setzer
Indexed induction-recursion. J. Log. Algebraic Methods Program. 66 (1) (2006)
Gilles Barthe, Peter Dybjer, Peter Thiemann
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. J. Funct. Program. 14 (1) (2004)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Inf. Softw. Technol. 46 (15) (2004)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
Random Generators for Dependent Types. ICTAC (2004)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
Verifying Haskell Programs by Combining Testing and Proving. QSIC (2003)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
Combining Testing and Proving in Dependent Type Theory. TPHOLs (2003)
Marcin Benke, Peter Dybjer, Patrik Jansson
Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput. 10 (4) (2003)
Peter Dybjer, Anton Setzer
Induction-recursion and initial algebras. Ann. Pure Appl. Log. 124 (1-3) (2003)
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS (2001)
Peter Dybjer, Anton Setzer
Indexed Induction-Recursion. Proof Theory in Computer Science (2001)
Peter Dybjer, Andrzej Filinski
Normalization and Partial Evaluation. APPSEM (2000)
Peter Dybjer
A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. 65 (2) (2000)
Peter Dybjer, Anton Setzer
A Finite Axiomatization of Inductive-Recursive Definitions. TLCA (1999)
Djordje Cubric, Peter Dybjer, Philip J. Scott
Normalization and the Yoneda Embedding. Math. Struct. Comput. Sci. 8 (2) (1998)
Peter Dybjer
Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. Theor. Comput. Sci. 176 (1-2) (1997)
Thierry Coquand, Peter Dybjer
Intuitionistic Model Constructions and Normalization Proofs. Math. Struct. Comput. Sci. 7 (1) (1997)
Sten Agerholm, Ilya Beylin, Peter Dybjer
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. TPHOLs (1996)
Ilya Beylin, Peter Dybjer
Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES (1995)
Peter Dybjer
Internal Type Theory. TYPES (1995)
Thierry Coquand, Peter Dybjer
Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS (1994)
Peter Dybjer
Inductive Families. Formal Aspects Comput. 6 (4) (1994)
Peter Dybjer
Inverse Image Analysis Generalises Strictness Analysis Inf. Comput. 90 (2) (1991)
Peter Dybjer
Comparing Integrated and External Logics of Functional Programs. Sci. Comput. Program. 14 (1) (1990)
Peter Dybjer, Herbert P. Sander
A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Formal Aspects Comput. 1 (4) (1989)
Peter Dybjer, Herbert P. Sander
A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Specification and Verification of Concurrent Systems (1988)
Peter Dybjer
Inverse Image Analysis. ICALP (1987)
Peter Dybjer
Category Theory and Programming Language Semantics: an Overview. CTCS (1985)
Peter Dybjer
Program Verification in a Logical Theory of Constructions. FPCA (1985)
Peter Dybjer
Using Domain Algebras to Prove the Correctness of a Compiler. STACS (1985)
Peter Dybjer
Domain Algebras. ICALP (1984)
Peter Dybjer
Some Results on the Deductive Structure of Join Dependencies. Theor. Comput. Sci. 33 (1984)
Peter Dybjer
Towards a Unified Theory of Data Types: Some Categorical Aspects. ADT (1983)