Dr Nicolai Kraus

Dr Nicolai Kraus

School of Computer Science
Royal Society University Research Fellow

Contact details

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

Dr Nicolai Kraus is a Royal Society University Research Fellow and a member of the Theory Group in the School of Computer Science.

Nicolai received his PhD in Computer Science from the University of Nottingham in 2015. Afterwards, he held postdoctoral research positions in Nottingham and at the Eötvös Loránd University in Budapest, before joining the University of Birmingham in October 2019.

Qualifications

PhD in Computer Science, University of Nottingham, 2015.

Research

Nicolai’s research lies in the intersection of mathematics and computer science. His interests are in logic and dependent type theory, especially homotopy type theory; category theory and higher dimensional category theory; formalised mathematics; and constructive mathematics in general.

Publications

Recent publications

Article

Capriotti, P & Kraus, N 2018, 'Univalent higher categories via complete Semi-Segal types', Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 44, pp. 44:1-11:29. https://doi.org/10.1145/3158132

Kraus, N & Sattler, C 2015, 'Higher Homotopies in a Hierarchy of Univalent Universes', ACM Transactions on Computational Logic, vol. 16, no. 2, 18. https://doi.org/10.1145/2729979

Conference contribution

Kraus, N & von Raumer, J 2019, Path spaces of higher inductive types in homotopy type theory. in 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, Canada, 24/06/19. https://doi.org/10.1109/LICS.2019.8785661

Kaposi, A, Kovács, A & Kraus, N 2019, Shallow embedding of type theory is morally correct. in G Hutton (ed.), Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings., Chapter 12, Lecture Notes in Computer Science, vol. 11825, Springer, pp. 329-365, 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal, 7/10/19. https://doi.org/10.1007/978-3-030-33636-3_12

Kraus, N & Altenkirch, T 2018, Free higher groups in homotopy type theory. in Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018). Association for Computing Machinery (ACM), pp. 599-608, Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), Oxford, United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209183

Altenkirch, T, Capriotti, P, Dijkstra, G, Kraus, N & Nordvall Forsberg, F 2018, Quotient inductive-inductive types. in C Baier & U Dal Lago (eds), Foundations of Software Science and Computation Structures : 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Lecture Notes in Computer Science , vol. 10803 , Springer Verlag, pp. 293-310, 21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 14/04/18. https://doi.org/10.1007/978-3-319-89366-2_16

Altenkirch, T, Danielsson, NA & Kraus, N 2017, Partiality, revisited: The partiality monad as a quotient inductive-inductive type. in J Esparza & AS Murawski (eds), Foundations of Software Science and Computation Structures : 20th International Conference, FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Lecture Notes in Computer Science, vol. 10203, Springer, pp. 534-549, 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, Uppsala, Sweden, 22/04/17. https://doi.org/10.1007/978-3-662-54458-7_31

Kraus, N 2016, Constructions with non-recursive higher inductive types. in LICS '16 - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery (ACM), pp. 595-604, The 31st Annual ACM/IEEE Symposium on Logic in Computer Science , New York, United States, 5/07/16. https://doi.org/10.1145/2933575.2933586

Altenkirch, T, Capriotti, P & Kraus, N 2016, Extending homotopy type theory with strict equality. in J-M Talbot & L Regnier (eds), 25th EACSL Annual Conference on Computer Science Logic 2016 (CSL 2016)., 21, Leibniz International Proceedings in Informatics, LIPIcs, vol. 62, Schloss Dagstuhl, pp. 21:1-21:17, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic, Marseille, France, 29/08/16. https://doi.org/10.4230/LIPIcs.CSL.2016.21

Capriotti, P, Kraus, N & Vezzosi, A 2015, Functions out of higher truncations. in S Kreutzer (ed.), 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics, LIPIcs, vol. 41, Schloss Dagstuhl, pp. 359-373, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, Berlin, Germany, 7/09/15. https://doi.org/10.4230/LIPIcs.CSL.2015.359

Kraus, N 2015, The general universal property of the propositional truncation. in H Herbelin, P Letouzey & M Sozeau (eds), 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics, LIPIcs, vol. 39, Schloss Dagstuhl, pp. 111-145, 20th International Conference on Types for Proofs and Programs, TYPES 2014, Paris, France, 12/05/14. https://doi.org/10.4230/LIPIcs.TYPES.2014.111

View all publications in research portal