Edit Profile (opens in new tab) Dybjer, Peter Co-Author Distance Author ID: dybjer.peter Published as: Dybjer, Peter Homepage: http://www.cse.chalmers.se/~peterd/ External Links: ORCID · Google Scholar · ResearchGate · dblp · GND Documents Indexed: 44 Publications since 1982 8 Contributions as Editor · 1 Further Contribution Co-Authors: 37 Co-Authors with 38 Joint Publications 518 Co-Co-Authors all top 5 Co-Authors 15 single-authored 7 Coquand, Thierry 6 Clairambault, Pierre 4 Setzer, Anton 3 Abel, Andreas M. 3 Bove, Ana 3 Castellan, Simon 2 Bezem, Marc 2 Buisse, Alexandre 2 Hötzel Escardó, Martín 2 Nordström, Bengt 2 Palmgren, Erik 2 Pinto, Luís F. 2 Pitts, Andrew M. 2 Scott, Philip J. 2 Smith, Jan M. 1 Aczel, Peter 1 Aehlig, Klaus 1 Ahrens, Benedikt 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Barthe, Gilles 1 Bauer, Andrej 1 Benke, Marcin 1 Bertot, Yves 1 Beylin, Ilya 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Cohen, Cyril 1 Constable, Robert Lee 1 Čubrić, Djordje 1 Curien, Pierre-Louis 1 Espírito Santo, José Carlos 1 Filinski, Andrzej 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Haiyan, Qiao 1 Hales, Thomas Callister 1 Harper, Robert 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hou (Favonia), Kuen-Bang 1 Jansson, Patrik 1 Joyal, André 1 Kapulkin, Krzysztof 1 Kock, Joachim 1 Kraus, Nicolai 1 Kuperberg, Denis 1 Li, Nuo 1 Licata, Dan 1 Lindström, Sten 1 Lumsdaine, Peter LeFanu 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Moeneclaey, Hugo 1 Nahas, Michael 1 Norell, Ulf 1 Pelayo, Alvaro 1 Pitt, David H. 1 Poigné, Axel 1 Polonsky, Andrew 1 Riehl, Emily 1 Rijke, Egbert 1 Rydeheard, David E. 1 Sander, Herbert P. 1 Saraiva, João Tomé 1 Scott, Dana Stewart 1 Shulman, Michael A. 1 Sicard-Ramírez, Andrés 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 Spitters, Bas 1 Sundholm, Göran 1 Swierstra, Wouter 1 Takeyama, Makoto 1 1 Van den Berg, Benno 1 Voevodskiĭ, Vladimir Aleksandrovich 1 Warren, Michael Alton 1 Zeilberger, Noam all top 5 Serials 4 MSCS. Mathematical Structures in Computer Science 4 Lecture Notes in Computer Science 2 Theoretical Computer Science 2 Annals of Pure and Applied Logic 2 Formal Aspects of Computing 1 The Journal of Symbolic Logic 1 Science of Computer Programming 1 Information and Computation 1 Nordic Journal of Computing 1 Journal of Functional Programming 1 The Journal of Logic and Algebraic Programming 1 Publications of the Newton Institute 1 Logic, Epistemology, and the Unity of Science 1 Logical Methods in Computer Science 1 LIPIcs – Leibniz International Proceedings in Informatics all top 5 Fields 38 Computer science (68-XX) 32 Mathematical logic and foundations (03-XX) 13 Category theory; homological algebra (18-XX) 7 General and overarching topics; collections (00-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Algebraic topology (55-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 43 Publications have been cited 382 times in 246 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Internal type theory. Zbl 1434.03149Dybjer, Peter 44 1996 Inductive families. Zbl 0808.03044Dybjer, Peter 42 1994 A brief overview of Agda – a functional language with dependent types. Zbl 1252.68062Bove, Ana; Dybjer, Peter; Norell, Ulf 40 2009 A general formulation of simultaneous inductive-recursive definitions in type theory. Zbl 0960.03048Dybjer, Peter 36 2000 Inductive sets and families in Martin-Löf’s type theory and their set- theoretic semantics. Zbl 0755.03033Dybjer, Peter 20 1991 Intuitionistic model constructions and normalization proofs. Zbl 0883.03009Coquand, Thierry; Dybjer, Peter 18 1997 A finite axiomatization of inductive-recursive definitions. Zbl 0931.03069Dybjer, Peter; Setzer, Anton 17 1999 Induction-recursion and initial algebras. Zbl 1044.03021Dybjer, Peter; Setzer, Anton 14 2003 Indexed induction-recursion. Zbl 1080.68014Dybjer, Peter; Setzer, Anton 12 2006 Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Zbl 0898.68047Dybjer, Peter 12 1997 The biequivalence of locally Cartesian closed categories and Martin-Löf type theories. Zbl 1342.03046Clairambault, Pierre; Dybjer, Peter 12 2014 Normalization and the Yoneda embedding. Zbl 0918.03012Čubrić, Djordje; Dybjer, Peter; Scott, Philip 12 1998 The biequivalence of locally Cartesian closed categories and Martin-Löf type theories. Zbl 1331.03045Clairambault, Pierre; Dybjer, Peter 11 2011 Universes for generic programs and proofs in dependent type theory. Zbl 1094.68012Benke, Marcin; Dybjer, Peter; Jansson, Patrik 8 2003 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 Dependent types at work. Zbl 1250.68086Bove, Ana; Dybjer, Peter 7 2009 Normalization and partial evaluation. Zbl 1065.68026Dybjer, Peter; Filinski, Andrzej 6 2002 Indexed induction-recursion. Zbl 1024.03062Dybjer, Peter; Setzer, Anton 6 2001 Finitary higher inductive types in the groupoid model. Zbl 07513458Dybjer, Peter; Moeneclaey, Hugo 6 2018 Comparing integrated and external logics of functional programs. Zbl 0699.68025Dybjer, Peter 5 1990 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 Undecidability of equality in the free locally Cartesian closed category (extended version). Zbl 1433.03028Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 4 2017 A functional programming approach to the specification and verification of concurrent systems. Zbl 0694.68015Dybjer, Peter; Sander, Herbert P. 3 1989 Inverse image analysis generalises strictness analysis. Zbl 0715.68052Dybjer, Peter 3 1991 Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. Zbl 1407.68432Beylin, Ilya; Dybjer, Peter 3 1996 Program testing and the meaning explanations of intuitionistic type theory. Zbl 1314.03032Dybjer, Peter 3 2012 Category theory and computer science. Manchester, UK, September 5–8, 1989. Proceedings. Zbl 0712.68006 3 1989 Using domain algebras to prove the correctness of a compiler. Zbl 0563.68012Dybjer, Peter 2 1985 Program verification in a logical theory of constructions. Zbl 0568.68015Dybjer, Peter 2 1985 Inductive definitions and type theory. An introduction (preliminary version). Zbl 1044.03521Coquand, Thierry; Dybjer, Peter 2 1994 Semantics and logics of computation. Summer school at the Isaac Newton Institute for Mathematical Sciences, Cambridge, GB, September 1995. Zbl 0894.00050 2 1997 Towards formalizing categorical models of type theory in type theory. Zbl 1278.03056Buisse, Alexandre; Dybjer, Peter 2 2008 Normalization by evaluation for Martin-Löf type theory with one universe. Zbl 1316.68038Abel, Andreas; Aehlig, Klaus; Dybjer, Peter 2 2007 Undecidability of equality in the free locally Cartesian closed category. Zbl 1433.03036Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 2 2015 Combining interactive and automatic reasoning in first order theories of functional programs. Zbl 1352.68038Bove, Ana; Dybjer, Peter; Sicard-Ramírez, Andrés 1 2012 Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046 1 2002 Random generators for dependent types. Zbl 1108.68498Dybjer, Peter; Haiyan, Qiao; Takeyama, Makoto 1 2005 Editorial: Special issue on programming with dependent types. Zbl 1418.68006 1 2017 Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Zbl 1248.03024Dybjer, Peter; Kuperberg, Denis 1 2012 The interpretation of intuitionistic type theory in locally Cartesian closed categories – an intuitionistic perspective. Zbl 1286.03029Buisse, Alexandre; Dybjer, Peter 1 2008 Categories with families: unityped, simply typed, and dependently typed. Zbl 1478.18001Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 1 2021 Game semantics and normalization by evaluation. Zbl 1459.68112Clairambault, Pierre; Dybjer, Peter 1 2015 Categories with families: unityped, simply typed, and dependently typed. Zbl 1478.18001Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 1 2021 Finitary higher inductive types in the groupoid model. Zbl 07513458Dybjer, Peter; Moeneclaey, Hugo 6 2018 Undecidability of equality in the free locally Cartesian closed category (extended version). Zbl 1433.03028Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 4 2017 Editorial: Special issue on programming with dependent types. Zbl 1418.68006 1 2017 Undecidability of equality in the free locally Cartesian closed category. Zbl 1433.03036Castellan, Simon; Clairambault, Pierre; Dybjer, Peter 2 2015 Game semantics and normalization by evaluation. Zbl 1459.68112Clairambault, Pierre; Dybjer, Peter 1 2015 The biequivalence of locally Cartesian closed categories and Martin-Löf type theories. Zbl 1342.03046Clairambault, Pierre; Dybjer, Peter 12 2014 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Program testing and the meaning explanations of intuitionistic type theory. Zbl 1314.03032Dybjer, Peter 3 2012 Combining interactive and automatic reasoning in first order theories of functional programs. Zbl 1352.68038Bove, Ana; Dybjer, Peter; Sicard-Ramírez, Andrés 1 2012 Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Zbl 1248.03024Dybjer, Peter; Kuperberg, Denis 1 2012 The biequivalence of locally Cartesian closed categories and Martin-Löf type theories. Zbl 1331.03045Clairambault, Pierre; Dybjer, Peter 11 2011 A brief overview of Agda – a functional language with dependent types. Zbl 1252.68062Bove, Ana; Dybjer, Peter; Norell, Ulf 40 2009 Dependent types at work. Zbl 1250.68086Bove, Ana; Dybjer, Peter 7 2009 Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. Zbl 1157.68025Abel, Andreas; Coquand, Thierry; Dybjer, Peter 8 2008 On the algebraic foundation of proof assistants for intuitionistic type theory. Zbl 1137.68570Abel, Andreas; Coquand, Thierry; Dybjer, Peter 5 2008 Towards formalizing categorical models of type theory in type theory. Zbl 1278.03056Buisse, Alexandre; Dybjer, Peter 2 2008 The interpretation of intuitionistic type theory in locally Cartesian closed categories – an intuitionistic perspective. Zbl 1286.03029Buisse, Alexandre; Dybjer, Peter 1 2008 Normalization by evaluation for Martin-Löf type theory with one universe. Zbl 1316.68038Abel, Andreas; Aehlig, Klaus; Dybjer, Peter 2 2007 Indexed induction-recursion. Zbl 1080.68014Dybjer, Peter; Setzer, Anton 12 2006 Random generators for dependent types. Zbl 1108.68498Dybjer, Peter; Haiyan, Qiao; Takeyama, Makoto 1 2005 Induction-recursion and initial algebras. Zbl 1044.03021Dybjer, Peter; Setzer, Anton 14 2003 Universes for generic programs and proofs in dependent type theory. Zbl 1094.68012Benke, Marcin; Dybjer, Peter; Jansson, Patrik 8 2003 Normalization and partial evaluation. Zbl 1065.68026Dybjer, Peter; Filinski, Andrzej 6 2002 Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046 1 2002 Indexed induction-recursion. Zbl 1024.03062Dybjer, Peter; Setzer, Anton 6 2001 A general formulation of simultaneous inductive-recursive definitions in type theory. Zbl 0960.03048Dybjer, Peter 36 2000 A finite axiomatization of inductive-recursive definitions. Zbl 0931.03069Dybjer, Peter; Setzer, Anton 17 1999 Normalization and the Yoneda embedding. Zbl 0918.03012Čubrić, Djordje; Dybjer, Peter; Scott, Philip 12 1998 Intuitionistic model constructions and normalization proofs. Zbl 0883.03009Coquand, Thierry; Dybjer, Peter 18 1997 Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Zbl 0898.68047Dybjer, Peter 12 1997 Semantics and logics of computation. Summer school at the Isaac Newton Institute for Mathematical Sciences, Cambridge, GB, September 1995. Zbl 0894.00050 2 1997 Internal type theory. Zbl 1434.03149Dybjer, Peter 44 1996 Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. Zbl 1407.68432Beylin, Ilya; Dybjer, Peter 3 1996 Inductive families. Zbl 0808.03044Dybjer, Peter 42 1994 Inductive definitions and type theory. An introduction (preliminary version). Zbl 1044.03521Coquand, Thierry; Dybjer, Peter 2 1994 Inductive sets and families in Martin-Löf’s type theory and their set- theoretic semantics. Zbl 0755.03033Dybjer, Peter 20 1991 Inverse image analysis generalises strictness analysis. Zbl 0715.68052Dybjer, Peter 3 1991 Comparing integrated and external logics of functional programs. Zbl 0699.68025Dybjer, Peter 5 1990 A functional programming approach to the specification and verification of concurrent systems. Zbl 0694.68015Dybjer, Peter; Sander, Herbert P. 3 1989 Category theory and computer science. Manchester, UK, September 5–8, 1989. Proceedings. Zbl 0712.68006 3 1989 Using domain algebras to prove the correctness of a compiler. Zbl 0563.68012Dybjer, Peter 2 1985 Program verification in a logical theory of constructions. Zbl 0568.68015Dybjer, Peter 2 1985 all cited Publications top 5 cited Publications all top 5 Cited by 323 Authors 17 Dybjer, Peter 8 Abel, Andreas M. 8 Coquand, Thierry 7 Ghani, Neil 7 Pitts, Andrew M. 6 Altenkirch, Thorsten 6 Palmgren, Erik 6 Setzer, Anton 5 Birkedal, Lars 5 Hötzel Escardó, Martín 5 Huber, Simon 5 Pientka, Brigitte 5 Popescu, Andrei 5 Sattler, Christian 4 Berger, Ulrich 4 Constable, Robert Lee 4 Fiore, Marcelo P. 4 Kunčar, Ondřej 4 McBride, Conor Thomas 4 van der Weide, Niels 3 Bickford, Mark 3 Bove, Ana 3 Chapman, James T. E. 3 Clouston, Ranald A. 3 Cohen, Liron 3 Gambino, Nicola 3 Garner, Richard 3 Gratzer, Daniel 3 Hancock, Peter G. 3 Hofmann, Martin 3 Jansson, Patrik 3 Kaposi, Ambrus 3 Klev, Ansten Mørch 3 Ko, Hsiang-Shang 3 Orton, Ian 3 Pagano, Miguel 3 Sacerdoti Coen, Claudio 3 Schwichtenberg, Helmut 3 Tassi, Enrico 2 Ahman, Danel 2 Ahrens, Benedikt 2 Allais, Guillaume 2 Angiuli, Carlo 2 Avigad, Jeremy 2 Backhouse, Roland C. 2 Barthe, Gilles 2 Biernacki, Dariusz 2 Bizjak, Aleš 2 Blanqui, Frédéric 2 Capretta, Venanzio 2 Clairambault, Pierre 2 de Moura, Leonardo 2 de Paiva, Valeria 2 Frumin, Dan 2 Fu, Yuxi 2 Geuvers, Jan Herman 2 Hedberg, Michael 2 Hutton, Graham 2 Kaliszyk, Cezary 2 Kapulkin, Krzysztof 2 Kavvos, G. A. 2 Kiselyov, Oleg 2 Kock, Joachim 2 Krauss, Alexander 2 Lumsdaine, Peter LeFanu 2 Luo, Zhaohui 2 Maggesi, Marco 2 Matthes, Ralph 2 Miller, Dale Allen 2 Møgelberg, Rasmus Ejlers 2 Mörtberg, Anders 2 Mu, Shin-Cheng 2 Nanevski, Aleksandar 2 Nordvall Forsberg, Fredrik 2 Pattinson, Dirk 2 Paulson, Lawrence Charles 2 Rabe, Florian 2 Rahli, Vincent 2 Sakurai, Takafumi 2 Schmidt, David A. 2 Schöpp, Ulrich 2 Schubert, Aleksy 2 Sestini, Filippo 2 Shan, Chung-chieh 2 Spitters, Bas 2 Sterling, Jonathan 2 Swierstra, Wouter 2 Uemura, Taichi 2 Urzyczyn, Paweł 2 Van den Berg, Benno 2 van Doorn, Floris 2 Veltri, Niccolò 2 Voevodskiĭ, Vladimir Aleksandrovich 2 von Raumer, Jakob 2 Weirich, Stephanie 2 Xu, Chuangjie 1 Ábrahám, Erika 1 Abramsky, Samson 1 Adelsberger, Stephan 1 Aehlig, Klaus ...and 223 more Authors all top 5 Cited in 40 Serials 23 MSCS. Mathematical Structures in Computer Science 20 Journal of Functional Programming 19 Theoretical Computer Science 14 Annals of Pure and Applied Logic 13 Logical Methods in Computer Science 11 Journal of Automated Reasoning 5 Information and Computation 4 Formal Aspects of Computing 4 RAIRO. Theoretical Informatics and Applications 3 Science of Computer Programming 3 Higher-Order and Symbolic Computation 2 The Journal of Symbolic Logic 2 Journal of Symbolic Computation 2 Journal of Computer Science and Technology 2 International Journal of Foundations of Computer Science 2 Archive for Mathematical Logic 2 The Journal of Logic and Algebraic Programming 2 ACM Transactions on Computational Logic 1 Acta Informatica 1 Artificial Intelligence 1 Mathematical Proceedings of the Cambridge Philosophical Society 1 Advances in Mathematics 1 Journal of the London Mathematical Society. Second Series 1 Journal of Pure and Applied Algebra 1 Notre Dame Journal of Formal Logic 1 Proceedings of the American Mathematical Society 1 Studia Logica 1 Synthese 1 Indagationes Mathematicae. New Series 1 The Bulletin of Symbolic Logic 1 Theory and Applications of Categories 1 Annals of Mathematics and Artificial Intelligence 1 Topoi 1 Journal of the European Mathematical Society (JEMS) 1 Fundamenta Informaticae 1 Sādhanā 1 Journal of Applied Logic 1 Mathematics in Computer Science 1 Journal of Formalized Reasoning 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 11 Fields 176 Computer science (68-XX) 148 Mathematical logic and foundations (03-XX) 46 Category theory; homological algebra (18-XX) 15 Algebraic topology (55-XX) 4 Order, lattices, ordered algebraic structures (06-XX) 2 General algebraic systems (08-XX) 2 General topology (54-XX) 1 General and overarching topics; collections (00-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year