Peter Dybjer - RankMe

67 papers A* 4A 1B 6C 1Misc 1Journal 27Unranked 20

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2024	J	`jnl`	The extended predicative Mahlo universe in Martin-Löf type theory. J. Log. Comput. Peter Dybjer, Anton Setzer
2022	J	`jnl`	Type Theories with Universe Level Judgements. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2022	—	`conf`	Type Theory with Explicit Universe Polymorphism. TYPES Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2021	J	`jnl`	On generalized algebraic theories and categories with families. Math. Struct. Comput. Sci. Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2020	J	`jnl`	A Note on Generalized Algebraic Theories and Categories with Families. CoRR Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó
2019	—	`ed.`	24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18-21, 2018 TYPES Peter Dybjer, José Espírito Santo, Luís Pinto
2019	J	`jnl`	Categories with Families: Unityped, Simply Typed, and Dependently Typed. CoRR Simon Castellan, Pierre Clairambault, Peter Dybjer
2018	B	`conf`	Finitary Higher Inductive Types in the Groupoid Model. MFPS Peter Dybjer, Hugo Moeneclaey
2017	J	`jnl`	Special issue on Programming with Dependent Types Editorial. J. Funct. Program. Wouter Swierstra, Peter Dybjer
2017	J	`jnl`	Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). Log. Methods Comput. Sci. Simon Castellan, Pierre Clairambault, Peter Dybjer
2015	B	`conf`	Game Semantics and Normalization by Evaluation. FoSSaCS Pierre Clairambault, Peter Dybjer
2015	—	`conf`	Undecidability of Equality in the Free Locally Cartesian Closed Category. TLCA Simon Castellan, Pierre Clairambault, Peter Dybjer
2015	J	`jnl`	Undecidability of Equality in the Free Locally Cartesian Closed Category. CoRR Simon Castellan, Pierre Clairambault, Peter Dybjer
2014	J	`jnl`	The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Math. Struct. Comput. Sci. Pierre Clairambault, Peter Dybjer
2012	B	`conf`	Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. FoSSaCS Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez
2012	—	`book`	Epistemology versus Ontology - Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf Epistemology versus Ontology Peter Dybjer, Sten Lindström, Erik Palmgren, Göran Sundholm
2012	J	`jnl`	Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Log. Peter Dybjer, Denis Kuperberg
2012	—	`ch.`	Program Testing and the Meaning Explanations of Intuitionistic Type Theory. Epistemology versus Ontology Peter Dybjer
2011	J	`jnl`	Agda Implementors Meeting (NII Shonan Meeting 2011-2). NII Shonan Meet. Rep. Peter Dybjer, Yoshiki Kinoshita, Shin-Cheng Mu
2011	J	`jnl`	The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories CoRR Pierre Clairambault, Peter Dybjer
2011	—	`conf`	The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. TLCA Pierre Clairambault, Peter Dybjer
2009	—	`conf`	A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs Ana Bove, Peter Dybjer, Ulf Norell
2009	—	`conf`	Embedding a logical theory of constructions in Agda. PLPV Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez
2008	—	`conf`	Dependent Types at Work. LerNet ALFA Summer School Ana Bove, Peter Dybjer
2008	Misc	`conf`	On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS Andreas Abel, Thierry Coquand, Peter Dybjer
2008	B	`conf`	The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. MFPS Alexandre Buisse, Peter Dybjer
2008	B	`conf`	Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC Andreas Abel, Thierry Coquand, Peter Dybjer
2007	A*	`conf`	Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS Andreas Abel, Thierry Coquand, Peter Dybjer
2007	B	`conf`	Normalization by Evaluation for Martin-Löf Type Theory with One Universe. MFPS Andreas Abel, Klaus Aehlig, Peter Dybjer
2007	—	`conf`	Towards Formalizing Categorical Models of Type Theory in Type Theory. LFMTP@CADE Alexandre Buisse, Peter Dybjer
2006	J	`jnl`	Indexed induction-recursion. J. Log. Algebraic Methods Program. Peter Dybjer, Anton Setzer
2004	J	`jnl`	Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. J. Funct. Program. Gilles Barthe, Peter Dybjer, Peter Thiemann
2004	C	`conf`	Random Generators for Dependent Types. ICTAC Peter Dybjer, Qiao Haiyan, Makoto Takeyama
2004	J	`jnl`	Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Inf. Softw. Technol. Peter Dybjer, Qiao Haiyan, Makoto Takeyama
2003	—	`conf`	Combining Testing and Proving in Dependent Type Theory. TPHOLs Peter Dybjer, Qiao Haiyan, Makoto Takeyama
2003	J	`jnl`	Induction-recursion and initial algebras. Ann. Pure Appl. Log. Peter Dybjer, Anton Setzer
2003	J	`jnl`	Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput. Marcin Benke, Peter Dybjer, Patrik Jansson
2003	—	`conf`	Verifying Haskell Programs by Combining Testing and Proving. QSIC Peter Dybjer, Qiao Haiyan, Makoto Takeyama
2002	—	`ed.`	Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures APPSEM Gilles Barthe, Peter Dybjer, Luís Pinto, João Saraiva
2001	—	`conf`	Indexed Induction-Recursion. Proof Theory in Computer Science Peter Dybjer, Anton Setzer
2001	A*	`conf`	Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott
2000	J	`jnl`	A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. Peter Dybjer
2000	—	`conf`	Normalization and Partial Evaluation. APPSEM Peter Dybjer, Andrzej Filinski
2000	—	`ed.`	Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers TYPES Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith
1999	—	`conf`	A Finite Axiomatization of Inductive-Recursive Definitions. TLCA Peter Dybjer, Anton Setzer
1998	J	`jnl`	Normalization and the Yoneda Embedding. Math. Struct. Comput. Sci. Djordje Cubric, Peter Dybjer, Philip J. Scott
1997	J	`jnl`	Intuitionistic Model Constructions and Normalization Proofs. Math. Struct. Comput. Sci. Thierry Coquand, Peter Dybjer
1997	J	`jnl`	Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. Theor. Comput. Sci. Peter Dybjer
1996	—	`conf`	A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. TPHOLs Sten Agerholm, Ilya Beylin, Peter Dybjer
1995	—	`conf`	Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES Ilya Beylin, Peter Dybjer
1995	—	`conf`	Internal Type Theory. TYPES Peter Dybjer
1995	—	`ed.`	Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers TYPES Peter Dybjer, Bengt Nordström, Jan M. Smith
1994	—	`conf`	Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS Thierry Coquand, Peter Dybjer
1994	J	`jnl`	Inductive Families. Formal Aspects Comput. Peter Dybjer
1991	J	`jnl`	Inverse Image Analysis Generalises Strictness Analysis Inf. Comput. Peter Dybjer
1990	J	`jnl`	Comparing Integrated and External Logics of Functional Programs. Sci. Comput. Program. Peter Dybjer
1989	J	`jnl`	A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Formal Aspects Comput. Peter Dybjer, Herbert P. Sander
1989	—	`ed.`	Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings Category Theory and Computer Science David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné
1988	—	`conf`	A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Specification and Verification of Concurrent Systems Peter Dybjer, Herbert P. Sander
1987	A*	`conf`	Inverse Image Analysis. ICALP Peter Dybjer
1985	—	`conf`	Category Theory and Programming Language Semantics: an Overview. CTCS Peter Dybjer
1985	—	`conf`	Program Verification in a Logical Theory of Constructions. FPCA Peter Dybjer
1985	A	`conf`	Using Domain Algebras to Prove the Correctness of a Compiler. STACS Peter Dybjer
1984	A*	`conf`	Domain Algebras. ICALP Peter Dybjer
1984	J	`jnl`	Some Results on the Deductive Structure of Join Dependencies. Theor. Comput. Sci. Peter Dybjer
1983	—	`conf`	Towards a Unified Theory of Data Types: Some Categorical Aspects. ADT Peter Dybjer