Peter Dybjer

Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm (Eds.): Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Logic, Epistemology, and the Unity of Science 27, Springer 2012, isbn 978-94-007-4434-9

Peter Dybjer, Denis Kuperberg: Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Logic 163(2): 122-131 (2012)

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

Peter Dybjer: Program Testing and the Meaning Explanations of Intuitionistic Type Theory. Epistemology versus Ontology 2012: 215-241

Pierre Clairambault, Peter Dybjer: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. TLCA 2011: 91-106

Pierre Clairambault, Peter Dybjer: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. CoRR abs/1112.3456 (2011)

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

Ana Bove, Peter Dybjer, Ulf Norell: A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs 2009: 73-78

Alexandre Buisse, Peter Dybjer: Towards Formalizing Categorical Models of Type Theory in Type Theory. Electr. Notes Theor. Comput. Sci. 196: 137-151 (2008)

Alexandre Buisse, Peter Dybjer: The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. Electr. Notes Theor. Comput. Sci. 218: 21-32 (2008)

Andreas Abel, Thierry Coquand, Peter Dybjer: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13

Ana Bove, Peter Dybjer: Dependent Types at Work. LerNet ALFA Summer School 2008: 57-99

Andreas Abel, Thierry Coquand, Peter Dybjer: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56

Andreas Abel, Klaus Aehlig, Peter Dybjer: Normalization by Evaluation for Martin-Löf Type Theory with One Universe. Electr. Notes Theor. Comput. Sci. 173: 17-39 (2007)

Andreas Abel, Thierry Coquand, Peter Dybjer: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12

Peter Dybjer, Anton Setzer: Indexed induction-recursion. J. Log. Algebr. Program. 66(1): 1-49 (2006)

Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology 46(15): 1011-1025 (2004)

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

Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Random Generators for Dependent Types. ICTAC 2004: 341-355

Peter Dybjer, Anton Setzer: Induction-recursion and initial algebras. Ann. Pure Appl. Logic 124(1-3): 1-47 (2003)

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

Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Verifying Haskell Programs by Combining Testing and Proving. QSIC 2003: 272-279

Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Combining Testing and Proving in Dependent Type Theory. TPHOLs 2003: 188-203

Gilles Barthe, Peter Dybjer, Luis Pinto, João Saraiva (Eds.): Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures. Lecture Notes in Computer Science 2395, Springer 2002, isbn 3-540-44044-5

Peter Dybjer, Anton Setzer: Indexed Induction-Recursion. Proof Theory in Computer Science 2001: 93-113

Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott: Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS 2001: 303-310

Peter Dybjer: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. 65(2): 525-549 (2000)

Peter Dybjer, Andrzej Filinski: Normalization and Partial Evaluation. APPSEM 2000: 137-192

Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith (Eds.): Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers. Lecture Notes in Computer Science 1956, Springer 2000, isbn 3-540-41517-3

Peter Dybjer, Anton Setzer: A Finite Axiomatization of Inductive-Recursive Definitions. TLCA 1999: 129-146

Djordje Cubric, Peter Dybjer, Philip J. Scott: Normalization and the Yoneda Embedding. Mathematical Structures in Computer Science 8(2): 153-192 (1998)

Thierry Coquand, Peter Dybjer: Intuitionistic Model Constructions and Normalization Proofs. Mathematical Structures in Computer Science 7(1): 75-94 (1997)

Peter Dybjer: Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. Theor. Comput. Sci. 176(1-2): 329-335 (1997)

Sten Agerholm, Ilya Beylin, Peter Dybjer: A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. TPHOLs 1996: 17-32

Ilya Beylin, Peter Dybjer: Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES 1995: 47-61

Peter Dybjer: Internal Type Theory. TYPES 1995: 120-134

Peter Dybjer, Bengt Nordström, Jan M. Smith (Eds.): Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers. Lecture Notes in Computer Science 996, Springer 1995, isbn 3-540-60579-7

Peter Dybjer: Inductive Families. Formal Asp. Comput. 6(4): 440-465 (1994)

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

Peter Dybjer: Inverse Image Analysis Generalises Strictness Analysis. Inf. Comput. 90(2): 194-216 (1991)

Peter Dybjer: Comparing Integrated and External Logics of Functional Programs. Sci. Comput. Program. 14(1): 59-79 (1990)

Peter Dybjer, Herbert P. Sander: A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Formal Asp. Comput. 1(4): 303-319 (1989)

David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné (Eds.): Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings. Lecture Notes in Computer Science 389, Springer 1989, isbn 3-540-51662-X

Peter Dybjer, Herbert P. Sander: A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Specification and Verification of Concurrent Systems 1988: 331-343

Peter Dybjer: Inverse Image Analysis. ICALP 1987: 21-30

Peter Dybjer: Category Theory and Programming Language Semantics: an Overview. CTCS 1985: 165-181

Peter Dybjer: Program Verification in a Logical Theory of Constructions. FPCA 1985: 334-349

Peter Dybjer: Using Domain Algebras to Prove the Correctness of a Compiler. STACS 1985: 98-108

Peter Dybjer: Some Results on the Deductive Structure of Join Dependencies. Theor. Comput. Sci. 33: 95-105 (1984)

Peter Dybjer: Domain Algebras. ICALP 1984: 138-150

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