Benedikt Ahrens

Publications & preprints

• About me & Contact
• My Research Team
• Publications & preprints
• Talks
• Teaching
• CV
• Grants
• Supervision Work
• UniMath
• PhD Dissertation
• Scientific Activities
• Collaborators

Publications and preprints

• Univalent Monoidal Categories
  with K. Wullaert and R. Matthes
  arXiv:2212.03146

• Semantics for two-dimensional type theory
  with P. R. North and N. van der Weide
  • Proceedings of LICS 2022
    doi:10.1145/3531130.3533334
  • A longer version is available as arXiv:2201.10662

• Bicategories in Univalent Foundations
  with D. Frumin, M. Maggesi, and N. van der Weide
  arXiv:1903.01152
  • Journal version: Mathematical Structures in Computer Science
    doi:10.1017/S0960129522000032
  • Conference version: Formal Structures for Computation and Deduction (FSCD) 2019, LIPIcs Vol. 131, pp. 5:1-5:17
    doi:10.4230/LIPIcs.FSCD.2019.5

• Implementing a Category-Theoretic Framework for Typed Abstract Syntax
  with R. Matthes and A. Mörtberg
  Certified Programs and Proofs 2022
  doi:10.1145/3497775.3503678
  arXiv:2112.06984

• B-systems and C-systems are equivalent
  with J. Emmengger, P. R. North, and E. Rijke
  arXiv:2111.09948

• The solutions to single-variable polynomials, implemented and verified in Lean
  with N. Dyson and J. Emmenegger
  arXiv:2201.00255

• Presentable signatures and initial semantics
  with A. Hirschowitz, A. Lafont, and M. Maggesi
  arXiv:1805.03740v5
  • Journal version: Logical Methods in Computer Science,
    doi:10.23638/LMCS-17(2:17)2021
  • Conference version (with title High-level signatures and initial semantics):
    Computer Science Logic (CSL) 2018, LIPIcs Vol. 119, pp. 4:1-4:22
    doi:10.4230/LIPIcs.CSL.2018.4

• The Univalence Principle
  with P. R. North, M. Shulman, and D. Tsementzis
  arXiv:2102.06275
  This book supersedes the article titled “A Higher Structure Identity Principle”.

• A Higher Structure Identity Principle
  with P. R. North, M. Shulman, and D. Tsementzis
  Proceedings of Logic in Computer Science (LICS) 2020
  doi:10.1145/3373718.3394755
  arXiv:2004.06572 (longer version)

• Reduction Monads and Their Signatures
  with A. Hirschowitz, A. Lafont, and M. Maggesi
  Proceedings of the ACM on Programming Languages (PACMPL), POPL 2020
  doi:10.1145/3371099
  arXiv:1911.06391

• Modular specification of monads through higher-order presentations
  with A. Hirschowitz, A. Lafont, and M. Maggesi
  Formal Structures for Computation and Deduction (FSCD) 2019, LIPIcs Vol. 131, pp. 6:1-6:19
  doi:10.4230/LIPIcs.FSCD.2019.6
  arXiv:1903.00922

• Univalent foundations and the equivalence principle
  with P. R. North
  Chapter in Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts
  Synthese, Springer
  doi:10.1007/978-3-030-15655-8
  arXiv:2202.01892

• Initial Semantics for Reduction Rules
  Logical Methods in Computer Science,
  doi:10.23638/LMCS-15(1:28)2019
  arXiv:1212.5668
  Accompanying Coq code on Github

• Categorical structures for type theory in univalent foundations
  with P. Lumsdaine and V. Voevodsky
  arXiv:1705.04310
  • Journal version: Logical Methods in Computer Science,
    doi:10.23638/LMCS-14(3:18)2018
  • Conference version: Computer Science Logic (CSL) 2017, LIPIcs Vol. 82, pp. 8:1-8:16
    doi:10.4230/LIPIcs.CSL.2017.8

• Displayed categories
  with P. Lumsdaine
  arXiv:1705.04296
  • Journal version: Logical Methods in Computer Science,
    doi:10.23638/LMCS-15(1:20)2019
  • Conference version: Formal Structures for Computation and Deduction (FSCD) 2017
    doi:10.4230/LIPIcs.FSCD.2017.5

• From signatures to monads in UniMath
  with R. Matthes and A. Mörtberg
  Journal of Automated Reasoning, 2018 (open access)
  doi:10.1007/s10817-018-9474-4
  arXiv:1612.00693

• Heterogeneous substitution systems revisited
  with R. Matthes
  TYPES 2015 Postproceedings
  doi:10.4230/LIPIcs.TYPES.2015.2, LIPIcs Vol. 69, pp. 2:1-2:23
  arXiv:1601.04299

• Some wellfounded trees in UniMath—extended abstract
  with A. Mörtberg
  Proceedings of ICMS 2016, Springer LNCS 9725, pp. 9-17
  doi:10.1007/978-3-319-42432-3_2

• Modules over relative monads for syntax and semantics
  Mathematical Structures in Computer Science, Vol. 26, pp. 3-37, 2016
  doi:10.1017/S0960129514000103
  arXiv:1107.5252
  Accompanying Coq code on Github

• Non-wellfounded trees in Homotopy Type Theory
  with P. Capriotti and R. Spadotti
  Proceedings of TLCA 2015, LIPIcs Vol. 38, pp. 17-30
  doi:10.4230/LIPIcs.TLCA.2015.17
  project web page with Agda code

• Terminal semantics for codata types in intensional Martin-Löf type theory
  with R. Spadotti
  TYPES 2014 Postproceedings, LIPIcs Vol. 39, pp. 1-26
  doi:10.4230/LIPIcs.TYPES.2014.1
  arXiv:1401.1053
  project web page with Coq code

• Univalent categories and the Rezk completion
  with K. Kapulkin and M. Shulman
  Mathematical Structures in Computer Science, Vol. 25, pp. 1010-1039, 2015
  doi:10.1017/S0960129514000486
  arXiv:1303.0584
  Accompanying Coq code on Github

• Initiality for Typed Syntax and Semantics—extended abstract
  Proceedings of WoLLIC 2012. LNCS Vol. 7456, 127 – 141
  The original publication is available at www.springerlink.com.
  doi:10.1007/978-3-642-32621-9_10
  arXiv:1206.4547 (identical to Springer version)
  This extended abstract gives a summary of the results of my dissertation.

• Extended Initiality for Typed Abstract Syntax
  Logical Methods in Computer Science, Vol. 8, No. 2 (2012)
  Link to published version (open access)
  doi:10.2168/LMCS-8(2:1)2012
  arXiv:1107.4751

• Initial Semantics for higher-order typed syntax in Coq
  with J. Zsidó
  Journal of Formalized Reasoning, Vol. 4, No. 1 (2011)
  Link to published version (open access)
  doi:10.6092/issn.1972-5787/2066
  arXiv:1012.1010
  Accompanying Coq code on Github

Contributions to books

• Univalent categories and the Rezk completion
  with K. Kapulkin and M. Shulman
  In Extended Abstracts Fall 2013—Geometrical Analysis; Type Theory, Homotopy Theory and Univalent Foundations
  Eds.: M. del Mar González, P. C. Yang, N. Gambino, J. Kock
  Birkhäuser
  doi:10.1007/978-3-319-21284-5

• Homotopy Type Theory:
  Univalent Foundations of Mathematics
  Webpage of the HoTT book

Software

• UniMath - a computer-checked library of univalent mathematics
  with V. Voevodsky, D. Grayson, and many others
  Hosted in a Github repository
  More information is available on the dedicated site.

Extended abstracts

• Categorical structures for type theory in univalent foundations, II
  with N. Kudasov, P. L. Lumsdaine, and V. Voevodsky
  Presented at workshop HoTT/UF 2020

• Bicategories in Univalent Foundations
  with D. Frumin, M. Maggesi, and N. van der Weide
  Presented at workshop TYPES 2019

• A modular formalization of bicategories in type theory
  with M. Maggesi
  Presented at workshop TYPES 2018
  Abstract

• Non-wellfounded trees in Homotopy Type Theory
  with P. Capriotti and R. Spadotti
  Presented at workshop TYPES 2015
  Abstract

• Substitution systems revisited
  with R. Matthes
  Presented at workshop TYPES 2015
  Abstract

• Coinitial semantics for codata types in intensional Martin-Löf type theory
  with R. Spadotti
  Presented at workshops CMCS 2014 and TYPES 2014
  Abstract

• Univalent categories and the Rezk completion
  with K. Kapulkin and M. Shulman
  Presented at workshop TYPES 2013
  Abstract

• Initiality for typed syntax and semantics
  Presented at workshop TYPES 2011
  Abstract