Dr Benedikt Ahrens PhD

Dr Benedikt Ahrens

School of Computer Science
Birmingham Fellow

Contact details

Address
School of Computer Science
University of Birmingham
Edgbaston
Birmingham
B15 2TT
UK

Benedikt Ahrens is a Birmingham Fellow for the Theory of Computation group in the School of Computer Science.

Benedikt is working on categorical semantics of programming languages. He is also interested in interactive theorem proving, mostly in computer proof assistants based on dependent type theory.

 He is a developer of the UniMath library of formalized mathematics.

Please follow the link below to find out more about Benedikt's work:

Dr Benedikt Ahrens'-personal webpage

Qualifications

  • PhD in Mathematics in 2012, Université Nice Sophia Antipolis

  •  Master in Mathematics in 2008, Université Nice Sophia Antipolis 

Biography

Benedikt received his PhD in Mathematics from Université Nice Sophia Antipolis. Afterwards, he held postdoctoral research fellowships at the Institute for Advanced Study, Princeton, NJ, at the International Centre for Mathematics and Computer Science in Toulouse, France, and at Inria, Nantes, France.

Teaching

  • Logic and Computation 

Postgraduate supervision

  • Semantics and type theory 

Research

Benedikt’s research lies at the intersection of mathematics and computer science. He studies univalent foundations of mathematics and semantics of programming languages. Benedikt strives to check his proofs mechanically in a computer proof assistant.

Publications

Recent publications

Article

Ahrens, B, Emmenegger, J, North, PR & Rijke, E 2023, 'B-systems and C-systems are equivalent', Journal of Symbolic Logic. https://doi.org/10.1017/jsl.2023.41

Ahrens, B, North, PR & van der Weide, N 2023, 'Bicategorical type theory: semantics and syntax', Mathematical Structures in Computer Science. https://doi.org/10.1017/S0960129523000312

Ahrens, B, Frumin, D, Maggesi, M, Veltri, N & Van Der Weide, N 2022, 'Bicategories in univalent foundations', Mathematical Structures in Computer Science. https://doi.org/10.1017/S0960129522000032

Ahrens, B, Hirschowitz, A, Lafont, A & Maggesi, M 2021, 'Presentable signatures and initial semantics', Logical Methods in Computer Science, vol. 17, no. 2, pp. 17:1–17:28. https://doi.org/10.23638/LMCS-17(2:17)2021

Ahrens, B & Lumsdaine, PL 2019, 'Displayed Categories', Logical Methods in Computer Science, vol. 15, no. 1, 20. https://doi.org/10.23638/LMCS-15(1:20)2019

Ahrens, B, Matthes, R & Mörtberg, A 2019, 'From signatures to monads in UniMath', Journal of Automated Reasoning, vol. 63, no. 2, pp. 285-318. https://doi.org/10.1007/s10817-018-9474-4

Ahrens, B 2019, 'Initial semantics for reduction rules', Logical Methods in Computer Science, vol. 15, no. 1, pp. 28:1-28:45. https://doi.org/10.23638/LMCS-15(1:28)2019

Ahrens, B, Lumsdaine, PL & Voevodsky, V 2018, 'Categorical structures for type theory in univalent foundations', Logical Methods in Computer Science, vol. 14, no. 3, 18. https://doi.org/10.23638/LMCS-14(3:18)2018

Chapter (peer-reviewed)

Ahrens, B & Randall North, P 2019, Univalent foundations and the equivalence principle. in S Centrone , D Kant & D Sarikaya (eds), Reflections on the Foundations of Mathematics. vol. 407, Synthese Library, Springer, pp. 137-150. https://doi.org/10.1007/978-3-030-15655-8_6

Conference article

Ahrens, B, Hirschowitz, A, Lafont, A & Maggesi, M 2020, 'Reduction Monads and Their Signatures', Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, 31. https://doi.org/10.1145/3371099

Conference contribution

Ahrens, B, Matthes, R & Mörtberg, A 2022, Implementing a category-theoretic framework for typed abstract syntax. in A Popescu & S Zdancewic (eds), CPP '22: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery (ACM), pp. 307-323, CPP '22, Philadelphia , Pennsylvania, United States, 17/01/22. https://doi.org/10.1145/3497775.3503678

Ahrens, B, North, PR & Van Der Weide, N 2022, Semantics for two-dimensional type theory. in LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, Association for Computing Machinery (ACM), 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Haifa, Israel, 2/08/22. https://doi.org/10.1145/3531130.3533334

Ahrens, B, Randall North, P, Shulman, M & Tsementzis, D 2020, A Higher Structure Identity Principle. in 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020). IEEE Computer Society Press, 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), Online, 8/07/20.

Ahrens, B, Frumin, D, Maggesi, M & van der Weide, N 2019, Bicategories in univalent foundations. in H Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)., 5, Leibniz International Proceedings in Informatics, LIPIcs, vol. 131, Schloss Dagstuhl, pp. 5:1-5:17, International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Dortmund, Germany, 24/06/19. https://doi.org/10.4230/LIPIcs.FSCD.2019.5

Ahrens, B, Hirschowitz, A, Lafont, A & Maggesi, M 2019, Modular specification of monads through higher-order presentations. in H Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)., 6, Leibniz International Proceedings in Informatics, LIPIcs, vol. 131, Schloss Dagstuhl, pp. 6:1-6:19, International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Dortmund, Germany, 24/06/19. https://doi.org/10.4230/LIPIcs.FSCD.2019.6

View all publications in research portal