Peter Dybjer - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 55 from 55

2022

Type Theory with Explicit Universe PolymorphismMarc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó. TYPES 2023: [doi]

2021

On generalized algebraic theories and categories with familiesMarc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó. mscs, 31(9):1006-1023, 2021. [doi]

2018

Finitary Higher Inductive Types in the Groupoid ModelPeter Dybjer, Hugo Moeneclaey. ENTCS, 336:119-134, 2018. [doi]

2017

Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)Simon Castellan, Pierre Clairambault, Peter Dybjer. lmcs, 13(4), 2017. [doi]

Special issue on Programming with Dependent Types EditorialWouter Swierstra, Peter Dybjer. JFP, 27, 2017. [doi]

2015

Undecidability of Equality in the Free Locally Cartesian Closed CategorySimon Castellan, Pierre Clairambault, Peter Dybjer. tlca 2015: 138-152 [doi]

Game Semantics and Normalization by EvaluationPierre Clairambault, Peter Dybjer. fossacs 2015: 56-70 [doi]

2014

The biequivalence of locally cartesian closed categories and Martin-Löf type theoriesPierre Clairambault, Peter Dybjer. mscs, 24(6), 2014. [doi]

2013

The biequivalence of locally cartesian closed categories and Martin-Löf type theoriesPierre Clairambault, Peter Dybjer. mscs, 24(5), 2013. [doi]

2012

Combining Interactive and Automatic Reasoning in First Order Theories of Functional ProgramsAna Bove, Peter Dybjer, Andrés Sicard-Ramírez. fossacs 2012: 104-118 [doi]

Program Testing and the Meaning Explanations of Intuitionistic Type TheoryPeter Dybjer. In Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm, editors, Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Volume 27 of Logic, Epistemology, and the Unity of Science, pages 215-241, Springer, 2012. [doi]

Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluationPeter Dybjer, Denis Kuperberg. APAL, 163(2):122-131, 2012. [doi]

2011

The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type TheoriesPierre Clairambault, Peter Dybjer. tlca 2011: 91-106 [doi]

Agda Implementors Meeting (NII Shonan Meeting 2011-2)Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu. shonan-reports, 2011, 2011. [doi]

2009

A Brief Overview of Agda - A Functional Language with Dependent TypesAna Bove, Peter Dybjer, Ulf Norell. tphol 2009: 73-78 [doi]

Embedding a logical theory of constructions in AgdaAna Bove, Peter Dybjer, AndrÃ©s Sicard-RamÃrez. plpv 2009: 59-66 [doi]

2008

2007

Normalization by Evaluation for Martin-Löf Type Theory with One UniverseAndreas Abel, Klaus Aehlig, Peter Dybjer. ENTCS, 173:17-39, 2007. [doi]

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality JudgementsAndreas Abel, Thierry Coquand, Peter Dybjer. lics 2007: 3-12 [doi]

2006

Indexed induction-recursionPeter Dybjer, Anton Setzer. jlp, 66(1):1-49, 2006. [doi]

2004

Introduction to the Special Issue on Dependent Type Theory Meets Practical ProgrammingGilles Barthe, Peter Dybjer, Peter Thiemann. JFP, 14(1):1-2, 2004. [doi]

Random Generators for Dependent TypesPeter Dybjer, Qiao Haiyan, Makoto Takeyama. ictac 2005: 341-355 [doi]

Verifying Haskell programs by combining testing, model checking and interactive theorem provingPeter Dybjer, Qiao Haiyan, Makoto Takeyama. INFSOF, 46(15):1011-1025, 2004. [doi]

2003

2001

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

Indexed Induction-RecursionPeter Dybjer, Anton Setzer. Dagstuhl 2001: 93-113 [doi]

2000

Normalization and Partial EvaluationPeter Dybjer, Andrzej Filinski. ac 2002: 137-192 [doi]

A General Formulation of Simultaneous Inductive-Recursive Definitions in Type TheoryPeter Dybjer. JSYML, 65(2):525-549, 2000.

1999

A Finite Axiomatization of Inductive-Recursive DefinitionsPeter Dybjer, Anton Setzer. tlca 1999: 129-146 [doi]

1998

Normalization and the Yoneda EmbeddingDjordje Cubric, Peter Dybjer, Philip J. Scott. mscs, 8(2):153-192, 1998.

1997

Intuitionistic Model Constructions and Normalization ProofsThierry Coquand, Peter Dybjer. mscs, 7(1):75-94, 1997.

Representing Inductively Defined Sets by Wellorderings in Martin-Löf s Type TheoryPeter Dybjer. TCS, 176(1-2):329-335, 1997. [doi]

1996

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

1995

Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for MonoidsIlya Beylin, Peter Dybjer. TYPES 1996: 47-61 [doi]

Internal Type TheoryPeter Dybjer. TYPES 1996: 120-134 [doi]

1994

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

Inductive FamiliesPeter Dybjer. fac, 6(4):440-465, 1994.

1991

Inverse Image Analysis Generalises Strictness AnalysisPeter Dybjer. iandc, 90(2):194-216, February 1991.

1990

Comparing Integrated and External Logics of Functional ProgramsPeter Dybjer. SCP, 14(1):59-79, 1990.

1989

A Functional Programming Approach to the Specification and Verification of Concurrent SystemsPeter Dybjer, Herbert P. Sander. fac, 1(4):303-319, 1989.

1988

A Functional Programming Approach to the Specification and Verification of Concurrent SystemsPeter Dybjer, Herbert P. Sander. facs 1990: 331-343

1987

Inverse Image AnalysisPeter Dybjer. icalp 1987: 21-30

1985

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

Program Verification in a Logical Theory of ConstructionsPeter Dybjer. fpca 1985: 334-349

Category Theory and Programming Language Semantics: an OverviewPeter Dybjer. ctcs 1986: 165-181

1984

Some Results on the Deductive Structure of Join DependenciesPeter Dybjer. TCS, 33:95-105, 1984.

Domain AlgebrasPeter Dybjer. icalp 1984: 138-150

1983

Towards a Unified Theory of Data Types: Some Categorical AspectsPeter Dybjer. adt 1983:

Sign in or sign up to see more results.

runs on WebDSL