default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDPeter Dybjer
Person information
- affiliation: Chalmers University of Technology, Gothenburg, Sweden
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j20]Peter Dybjer, Anton Setzer:
The extended predicative Mahlo universe in Martin-Löf type theory. J. Log. Comput. 34(6): 1032-1063 (2024)- 2022
- [c33]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
Type Theory with Explicit Universe Polymorphism. TYPES 2022: 13:1-13:16 - [i6]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
Type Theories with Universe Level Judgements. CoRR abs/2212.03284 (2022) - 2021
- [j19]Marc Bezem, Thierry Coquand
, Peter Dybjer, Martín Escardó:
On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. 31(9): 1006-1023 (2021) - 2020
- [i5]Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó:
A Note on Generalized Algebraic Theories and Categories with Families. CoRR abs/2012.08370 (2020)
2010 – 2019
- 2019
- [e6]Peter Dybjer, José Espírito Santo, Luís Pinto:
24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal. LIPIcs 130, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2019, ISBN 978-3-95977-106-1 [contents] - [i4]Simon Castellan, Pierre Clairambault, Peter Dybjer:
Categories with Families: Unityped, Simply Typed, and Dependently Typed. CoRR abs/1904.00827 (2019) - 2018
- [c32]Peter Dybjer, Hugo Moeneclaey:
Finitary Higher Inductive Types in the Groupoid Model. MFPS 2018: 119-134 - 2017
- [j18]Wouter Swierstra, Peter Dybjer:
Special issue on Programming with Dependent Types Editorial. J. Funct. Program. 27: e15 (2017) - [j17]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) - 2015
- [c31]Pierre Clairambault, Peter Dybjer:
Game Semantics and Normalization by Evaluation. FoSSaCS 2015: 56-70 - [c30]Simon Castellan, Pierre Clairambault, Peter Dybjer:
Undecidability of Equality in the Free Locally Cartesian Closed Category. TLCA 2015: 138-152 - [i3]Simon Castellan, Pierre Clairambault, Peter Dybjer:
Undecidability of Equality in the Free Locally Cartesian Closed Category. CoRR abs/1504.03995 (2015) - 2014
- [j16]Pierre Clairambault, Peter Dybjer:
The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Math. Struct. Comput. Sci. 24(6) (2014) - 2012
- [j15]Peter Dybjer, Denis Kuperberg:
Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Log. 163(2): 122-131 (2012) - [c29]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 - [p1]Peter Dybjer:
Program Testing and the Meaning Explanations of Intuitionistic Type Theory. Epistemology versus Ontology 2012: 215-241 - [e5]Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm:
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 [contents] - 2011
- [c28]Pierre Clairambault, Peter Dybjer:
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. TLCA 2011: 91-106 - [i2]Pierre Clairambault, Peter Dybjer:
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. CoRR abs/1112.3456 (2011) - [i1]Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu:
Agda Implementors Meeting (NII Shonan Meeting 2011-2). NII Shonan Meet. Rep. 2011 (2011)
2000 – 2009
- 2009
- [c27]Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez:
Embedding a logical theory of constructions in Agda. PLPV 2009: 59-66 - [c26]Ana Bove, Peter Dybjer, Ulf Norell:
A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs 2009: 73-78 - 2008
- [c25]Andreas Abel, Thierry Coquand, Peter Dybjer:
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13 - [c24]Ana Bove, Peter Dybjer:
Dependent Types at Work. LerNet ALFA Summer School 2008: 57-99 - [c23]Andreas Abel, Thierry Coquand, Peter Dybjer:
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56 - [c22]Alexandre Buisse, Peter Dybjer:
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. MFPS 2008: 21-32 - 2007
- [c21]Andreas Abel, Thierry Coquand, Peter Dybjer:
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12 - [c20]Andreas Abel, Klaus Aehlig, Peter Dybjer:
Normalization by Evaluation for Martin-Löf Type Theory with One Universe. MFPS 2007: 17-39 - [c19]Alexandre Buisse, Peter Dybjer:
Towards Formalizing Categorical Models of Type Theory in Type Theory. LFMTP@CADE 2007: 137-151 - 2006
- [j14]Peter Dybjer, Anton Setzer:
Indexed induction-recursion. J. Log. Algebraic Methods Program. 66(1): 1-49 (2006) - 2004
- [j13]Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Inf. Softw. Technol. 46(15): 1011-1025 (2004) - [j12]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) - [c18]Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
Random Generators for Dependent Types. ICTAC 2004: 341-355 - 2003
- [j11]Peter Dybjer, Anton Setzer:
Induction-recursion and initial algebras. Ann. Pure Appl. Log. 124(1-3): 1-47 (2003) - [j10]Marcin Benke, Peter Dybjer, Patrik Jansson:
Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput. 10(4): 265-289 (2003) - [c17]Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
Verifying Haskell Programs by Combining Testing and Proving. QSIC 2003: 272-279 - [c16]Peter Dybjer, Qiao Haiyan, Makoto Takeyama:
Combining Testing and Proving in Dependent Type Theory. TPHOLs 2003: 188-203 - 2002
- [e4]Gilles Barthe, Peter Dybjer, Luís Pinto, João Saraiva:
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 [contents] - 2001
- [c15]Peter Dybjer, Anton Setzer:
Indexed Induction-Recursion. Proof Theory in Computer Science 2001: 93-113 - [c14]Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott:
Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS 2001: 303-310 - 2000
- [j9]Peter Dybjer:
A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. 65(2): 525-549 (2000) - [c13]Peter Dybjer, Andrzej Filinski:
Normalization and Partial Evaluation. APPSEM 2000: 137-192 - [e3]Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith:
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 [contents]
1990 – 1999
- 1999
- [c12]Peter Dybjer, Anton Setzer:
A Finite Axiomatization of Inductive-Recursive Definitions. TLCA 1999: 129-146 - 1998
- [j8]Djordje Cubric, Peter Dybjer, Philip J. Scott:
Normalization and the Yoneda Embedding. Math. Struct. Comput. Sci. 8(2): 153-192 (1998) - 1997
- [j7]Thierry Coquand, Peter Dybjer:
Intuitionistic Model Constructions and Normalization Proofs. Math. Struct. Comput. Sci. 7(1): 75-94 (1997) - [j6]Peter Dybjer:
Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. Theor. Comput. Sci. 176(1-2): 329-335 (1997) - 1996
- [c11]Sten Agerholm, Ilya Beylin, Peter Dybjer:
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. TPHOLs 1996: 17-32 - 1995
- [c10]Ilya Beylin, Peter Dybjer:
Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES 1995: 47-61 - [c9]Peter Dybjer:
Internal Type Theory. TYPES 1995: 120-134 - [e2]Peter Dybjer, Bengt Nordström, Jan M. Smith:
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 [contents] - 1994
- [j5]Peter Dybjer:
Inductive Families. Formal Aspects Comput. 6(4): 440-465 (1994) - [c8]Thierry Coquand, Peter Dybjer:
Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS 1994: 60-76 - 1991
- [j4]Peter Dybjer:
Inverse Image Analysis Generalises Strictness Analysis. Inf. Comput. 90(2): 194-216 (1991) - 1990
- [j3]Peter Dybjer:
Comparing Integrated and External Logics of Functional Programs. Sci. Comput. Program. 14(1): 59-79 (1990)
1980 – 1989
- 1989
- [j2]Peter Dybjer, Herbert P. Sander:
A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Formal Aspects Comput. 1(4): 303-319 (1989) - [e1]David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné:
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 [contents] - 1988
- [c7]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 - 1987
- [c6]Peter Dybjer:
Inverse Image Analysis. ICALP 1987: 21-30 - 1985
- [c5]Peter Dybjer:
Category Theory and Programming Language Semantics: an Overview. CTCS 1985: 165-181 - [c4]Peter Dybjer:
Program Verification in a Logical Theory of Constructions. FPCA 1985: 334-349 - [c3]Peter Dybjer:
Using Domain Algebras to Prove the Correctness of a Compiler. STACS 1985: 98-108 - 1984
- [j1]Peter Dybjer:
Some Results on the Deductive Structure of Join Dependencies. Theor. Comput. Sci. 33: 95-105 (1984) - [c2]Peter Dybjer:
Domain Algebras. ICALP 1984: 138-150 - 1983
- [c1]Peter Dybjer:
Towards a Unified Theory of Data Types: Some Categorical Aspects. ADT 1983
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-16 21:27 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
