Dr Benedikt Ahrens PhD

School of Computer Science

Contact details

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

Benedikt Ahrens is a Birmingham Fellow for the Theory 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.

For more information, please visit Benedikt's Computer Science Profile

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, 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.

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, Lumsdaine, PL & Voevodsky, V 2018, 'Categorical structures for type theory in univalent foundations', Logical Methods in Computer Science, vol. 14, no. 3, 4814. https://doi.org/10.23638/LMCS-14(3:18)2018

Ahrens, B & Randall North, P 2018, 'Univalent Foundations and the Equivalence Principle', Synthese.

Ahrens, B 2016, 'Modules over relative monads for syntax and semantics', Mathematical Structures in Computer Science, vol. 26, no. 1, pp. 3-37. https://doi.org/10.1017/S0960129514000103

Conference contribution

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

Ahrens, B, Hirschowitz, A, Lafont, A & Maggesi, M 2018, High-level signatures and initial semantics. in DR Ghica & A Jung (eds), 27th EACSL Annual Conference on Computer Science Logic 2018 (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 119, Schloss Dagstuhl, pp. 4:1 - 4:22, 27th EACSL Annual Conference on Computer Science Logic 2018 (CSL 2018), Birmingham, United Kingdom, 4/09/18. https://doi.org/10.4230/LIPIcs.CSL.2018.4

Ahrens, B & Matthes, R 2018, Heterogeneous substitution systems revisited. in T Uustalu (ed.), 21st International Conference on Types and Proofs and Programs - TYPES 2015 - Postproceedings. vol. 69, Leibniz International Proceedings in Informatics (LIPIcs), vol. 69, Schloss Dagstuhl, pp. 2:1 - 2:23, 21st International Conference on Types and Proofs and Programs (TYPES 2015), Tallinn, Estonia, 18/05/15. https://doi.org/10.4230/LIPIcs.TYPES.2015.2

Ahrens, B & Lumsdaine, PL 2017, Displayed Categories. in D Miller (ed.), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). vol. 84, Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, Schloss Dagstuhl, pp. 5:1–5:16, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Oxford, United Kingdom, 3/09/17. https://doi.org/10.4230/LIPIcs.FSCD.2017.5

Ahrens, B, Lumsdaine, PL & Voevodsky, V 2017, Categorical structures for type theory in univalent foundations. in V Goranko & M Dam (eds), 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). vol. 82, Leibniz International Proceedings in Informatics (LIPIcs), vol. 82, Schloss Dagstuhl, Leibniz International Proceedings in Informatics, pp. 8:1–8:16, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden, 20/08/17. https://doi.org/10.4230/LIPIcs.CSL.2017.8

Ahrens, B & Mörtberg, A 2016, Some wellfounded trees in UniMath. in G-M Greuel, T Koch, P Paule & A Sommese (eds), Mathematical Software - ICMS 2016 : 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings. vol. 9725, Lecture Notes in Computer Science , vol. 9725, Springer Verlag, pp. 9-17, 5th International Conference on Mathematical Software, ICMS 2016, Berlin, Germany, 11/07/16. https://doi.org/10.1007/978-3-319-42432-3_2

Ahrens, B & Spadotti, R 2015, Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. in H Herbelin, P Letouzey & M Sozeau (eds), 20th International Conference on Types for Proofs and Programs (TYPES 2014). vol. 39, Leibniz International Proceedings in Informatics (LIPIcs), vol. 39, Schloss Dagstuhl, pp. 1-26, 20th International Conference on Types for Proofs and Programs (TYPES’14), Paris, France, 12/05/14. https://doi.org/10.4230/LIPIcs.TYPES.2014.1

Ahrens, B, Capriotti, P & Spadotti, R 2015, Non-wellfounded trees in homotopy type theory. in T Altenkirch (ed.), 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). vol. 38, Leibniz International Proceedings in Informatics (LIPIcs), vol. 38, Schloss Dagstuhl, Leibniz International Proceedings in Informatics, pp. 17-30, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Warsaw, Poland, 1/07/15. https://doi.org/10.4230/LIPIcs.TLCA.2015.17

View all publications in research portal