Edit Profile (opens in new tab) Ahrens, Benedikt Co-Author Distance Author ID: ahrens.benedikt Published as: Ahrens, Benedikt Homepage: https://benediktahrens.net External Links: MGP · ORCID · Google Scholar · dblp · IdRef · theses.fr Documents Indexed: 23 Publications since 2011 2 Contributions as Editor · 1 Further Contribution Co-Authors: 18 Co-Authors with 21 Joint Publications 171 Co-Co-Authors all top 5 Co-Authors 5 single-authored 5 Lumsdaine, Peter LeFanu 5 Maggesi, Marco 4 Mörtberg, Anders 3 Hirschowitz, André 3 Lafont, Ambroise 3 Shulman, Michael A. 3 Voevodskiĭ, Vladimir Aleksandrovich 2 Frumin, Dan 2 Huber, Simon 2 Kapulkin, Krzysztof 2 Matthes, Ralph 2 North, Paige Randall 2 Spadotti, Régis 2 van der Weide, Niels 1 Aczel, Peter 1 Altenkirch, Thorsten 1 Angiuli, Carlo 1 Avigad, Jeremy 1 Awodey, Steve 1 Barras, Bruno 1 Bauer, Andrej 1 Bertot, Yves 1 Bezem, Marc 1 Bordg, Anthony 1 Brunerie, Guillaume 1 Capriotti, Paolo 1 Cohen, Cyril 1 Constable, Robert Lee 1 Coquand, Thierry 1 Curien, Pierre-Louis 1 Dybjer, Peter 1 Finster, Eric 1 Gambino, Nicola 1 Garner, Richard 1 Gonthier, Georges 1 Grayson, Daniel Richard 1 Hales, Thomas Callister 1 Harper, Robert 1 Herbelin, Hugo 1 Hofmann, Martin 1 Hofstra, Pieter J. W. 1 Hötzel Escardó, Martín 1 Hou (Favonia), Kuen-Bang 1 Joyal, André 1 Kock, Joachim 1 Kraus, Nicolai 1 Li, Nuo 1 Licata, Dan 1 Luo, Zhaohui 1 Mahboubi, Assia 1 Martin-Löf, Per 1 Melikhov, Sergey Aleksandrovich 1 Nahas, Michael 1 Palmgren, Erik 1 Pelayo, Alvaro 1 Polonsky, Andrew 1 Riehl, Emily 1 Rijke, Egbert 1 Scott, Dana Stewart 1 Scott, Philip J. 1 Sojakova, Kristina 1 Solov’ëv, Sergeĭ Vladimirovich 1 Sozeau, Matthieu 1 Spitters, Bas 1 1 Tsementzis, Dimitris 1 Van den Berg, Benno 1 Veltri, Niccolò 1 Warren, Michael Alton 1 Zeilberger, Noam 1 Zsidó, Julianna Serials 5 MSCS. Mathematical Structures in Computer Science 5 Logical Methods in Computer Science 2 Journal of Formalized Reasoning 1 Journal of Automated Reasoning Fields 19 Mathematical logic and foundations (03-XX) 17 Computer science (68-XX) 16 Category theory; homological algebra (18-XX) 6 Algebraic topology (55-XX) 2 General and overarching topics; collections (00-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 15 Publications have been cited 59 times in 31 Documents Cited by ▼ Year ▼ Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Univalent categories and the Rezk completion. Zbl 1362.18003Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael 21 2015 Non-wellfounded trees in homotopy type theory. Zbl 1433.03027Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis 6 2015 Categorical structures for type theory in univalent foundations. Zbl 1496.03053Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir 6 2018 Displayed categories. Zbl 1419.18001Ahrens, Benedikt; Lefanu Lumsdaine, Peter 5 2019 Modules over relative monads for syntax and semantics. Zbl 1361.68034Ahrens, Benedikt 4 2016 Displayed categories. Zbl 1434.18002Ahrens, Benedikt; Lumsdaine, Peter LeFanu 3 2017 Heterogeneous substitution systems revisited. Zbl 1433.68220Ahrens, Benedikt; Matthes, Ralph 2 2018 Bicategories in univalent foundations. Zbl 07559271Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; van der Weide, Niels 2 2019 A higher structure identity principle. Zbl 1498.03027Ahrens, Benedikt; North, Paige Randall; Shulman, Michael; Tsementzis, Dimitris 2 2020 From signatures to monads in UniMath. Zbl 1468.03007Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 2 2019 Initial semantics for higher-order typed syntax in Coq. Zbl 1451.68312Ahrens, Benedikt; Zsido, Julianna 2 2011 Categorical structures for type theory in univalent foundations. Zbl 07204300Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir 2 2017 High-level signatures and initial semantics. Zbl 07533329Ahrens, Benedikt; Hirschowitz, André; Lafont, Ambroise; Maggesi, Marco 1 2018 Some wellfounded trees in UniMath (extended abstract). Zbl 1434.03023Ahrens, Benedikt; Mörtberg, Anders 1 2016 A higher structure identity principle. Zbl 1498.03027Ahrens, Benedikt; North, Paige Randall; Shulman, Michael; Tsementzis, Dimitris 2 2020 Displayed categories. Zbl 1419.18001Ahrens, Benedikt; Lefanu Lumsdaine, Peter 5 2019 Bicategories in univalent foundations. Zbl 07559271Ahrens, Benedikt; Frumin, Dan; Maggesi, Marco; van der Weide, Niels 2 2019 From signatures to monads in UniMath. Zbl 1468.03007Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders 2 2019 Categorical structures for type theory in univalent foundations. Zbl 1496.03053Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir 6 2018 Heterogeneous substitution systems revisited. Zbl 1433.68220Ahrens, Benedikt; Matthes, Ralph 2 2018 High-level signatures and initial semantics. Zbl 07533329Ahrens, Benedikt; Hirschowitz, André; Lafont, Ambroise; Maggesi, Marco 1 2018 Displayed categories. Zbl 1434.18002Ahrens, Benedikt; Lumsdaine, Peter LeFanu 3 2017 Categorical structures for type theory in univalent foundations. Zbl 07204300Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir 2 2017 Modules over relative monads for syntax and semantics. Zbl 1361.68034Ahrens, Benedikt 4 2016 Some wellfounded trees in UniMath (extended abstract). Zbl 1434.03023Ahrens, Benedikt; Mörtberg, Anders 1 2016 Univalent categories and the Rezk completion. Zbl 1362.18003Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael 21 2015 Non-wellfounded trees in homotopy type theory. Zbl 1433.03027Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis 6 2015 Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002The Univalent Foundations Program 122 2013 Initial semantics for higher-order typed syntax in Coq. Zbl 1451.68312Ahrens, Benedikt; Zsido, Julianna 2 2011 all cited Publications top 5 cited Publications all top 5 Cited by 39 Authors 12 Ahrens, Benedikt 5 Maggesi, Marco 4 van der Weide, Niels 3 Hirschowitz, André 3 Lafont, Ambroise 3 Lumsdaine, Peter LeFanu 3 Mörtberg, Anders 2 Buchholtz, Ulrik 2 Frumin, Dan 2 Matthes, Ralph 2 Veltri, Niccolò 2 Voevodskiĭ, Vladimir Aleksandrovich 1 Abel, Andreas M. 1 Bordg, Anthony 1 Castellan, Simon 1 Cavallo, Evan 1 Clairambault, Pierre 1 Coquand, Thierry 1 Danielsson, Nils Anders 1 Dutilh Novaes, Catarina 1 Dybjer, Peter 1 Geuvers, Jan Herman 1 Grayson, Daniel Richard 1 Harper, Robert 1 Hyvernat, Pierre 1 Kaposi, Ambrus 1 Kovács, András 1 Maietti, Maria Emilia 1 Maschio, Samuele 1 Navarro Garmendia, Alberto 1 North, Paige Randall 1 Rathjen, Michael 1 Riehl, Emily 1 Shulman, Michael A. 1 Stenzel, Raffael 1 Tsementzis, Dimitris 1 van Doorn, Floris 1 Vezzosi, Andrea 1 von Raumer, Jakob all top 5 Cited in 11 Serials 8 Logical Methods in Computer Science 2 Journal of Pure and Applied Algebra 2 Synthese 1 Journal of Automated Reasoning 1 MSCS. Mathematical Structures in Computer Science 1 Bulletin of the American Mathematical Society. New Series 1 Indagationes Mathematicae. New Series 1 Journal of Functional Programming 1 Theory and Applications of Categories 1 La Gaceta de la Real Sociedad Matemática Española 1 Higher Structures all top 5 Cited in 8 Fields 25 Mathematical logic and foundations (03-XX) 16 Category theory; homological algebra (18-XX) 14 Computer science (68-XX) 9 Algebraic topology (55-XX) 1 History and biography (01-XX) 1 General algebraic systems (08-XX) 1 Algebraic geometry (14-XX) 1 Group theory and generalizations (20-XX) Citations by Year