Bibliography for Nicolai Kraus
#28
@article{DEJONG2026108368,
title = {A study of Kock's fat Delta},
journal = {Journal of Pure and Applied Algebra},
volume = {230},
number = {11},
pages = {108368},
year = {2026},
issn = {0022-4049},
doi = {https://doi.org/10.1016/j.jpaa.2026.108368},
url = {https://www.sciencedirect.com/science/article/pii/S0022404926001994},
author = {Tom {de Jong} and Nicolai Kraus and Simona Paoli and Stiéphen Pradal},
abstract = {Motivated by the study of weak identity structures in higher category theory we explore the fat Delta category, a modification of the simplex category introduced by J. Kock and provide a comprehensive study via the theory of monads with arities. Specifically, by proving that the free relative semicategory monad is strongly cartesian and identifying a dense generator, the theory of monads with arities immediately gives rise to the nerve theorem. We characterise the essential image of the nerve via the Segal condition, and show that fat Delta possesses an active-inert factorisation system. Building on these results, we also establish an isomorphism between two presentations of fat Delta.}
}
#27
@InProceedings{dejong_et_al:LIPIcs.LICS.2026.59,
author = {de Jong, Tom and Kraus, Nicolai and Mohammadzadeh, Aref and Nordvall Forsberg, Fredrik},
title = {{Generalized Decidability via Brouwer Trees}},
booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)},
pages = {59:1--59:27},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-434-5},
ISSN = {1868-8969},
year = {2026},
volume = {380},
editor = {Faggian, Claudia and Katoen, Joost-Pieter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.59},
URN = {urn:nbn:de:0030-drops-268466},
doi = {10.4230/LIPIcs.LICS.2026.59},
annote = {Keywords: Decidability in constructive mathematics, homotopy type theory, ordinals, Brouwer trees, countable choice}
}
#26
@INPROCEEDINGS{tom-nicolai-fredrik-chuangjie:exponentiation,
author = {De Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie},
booktitle = {2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title = {Ordinal Exponentiation in Homotopy Type Theory},
year = {2025},
volume = {},
number = {},
pages = {262-274},
keywords = {Computer science;Logic;ordinal arithmetic;exponentiation;constructive mathematics;homotopy type theory;univalent foundations},
doi = {10.1109/LICS65433.2025.00027}
}
#25
@article{pierre-ulrik-nicolai-marc:spheres,
author = {Cagne, Pierre and Buchholtz, Ulrik and Kraus, Nicolai and Bezem, Marc},
journal = {ArXiv e-prints},
title = {On symmetries of spheres in univalent foundations},
year = {2024},
url = {https://arxiv.org/abs/2401.15037},
}
#24
@INPROCEEDINGS{dejong-kra-nf-xu:set-type-ordinals,
author={de Jong, Tom and Kraus, Nicolai and Norvall Forsberg, Fredrik and Xu, Chuangjie},
booktitle={2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title={Set-Theoretic and Type-Theoretic Ordinals Coincide},
year={2023},
volume={},
number={},
pages={1-13},
doi={10.1109/LICS56636.2023.10175762}
}
#23
@article{kra-nf-xu:ordinals,
title = {Type-theoretic approaches to ordinals},
journal = {Theoretical Computer Science},
volume = {957},
pages = {113843},
year = {2023},
issn = {0304-3975},
doi = {https://doi.org/10.1016/j.tcs.2023.113843},
url = {https://www.sciencedirect.com/science/article/pii/S0304397523001561},
author = {Nicolai Kraus and Fredrik {Nordvall Forsberg} and Chuangjie Xu},
note = {Preprint available as arXiv:2208.03844}
}
#22
@article{kraus_von raumer_2023,
title={A Rewriting Coherence Theorem with Applications in Homotopy Type Theory},
DOI={10.1017/S0960129523000026},
journal={Mathematical Structures in Computer Science},
publisher={Cambridge University Press},
author={Kraus, Nicolai and von Raumer, Jakob},
year={2023},
pages={1-33}
}
#21
@InProceedings{krausNordvallforsbergXu:ordinals,
author = {Kraus, Nicolai and Nordvall Forsberg, Fredrik and Xu, Chuangjie},
title = {{Connecting Constructive Notions of Ordinals in Homotopy Type Theory}},
booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
pages = {70:1--70:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-201-3},
ISSN = {1868-8969},
year = {2021},
volume = {202},
editor = {Bonchi, Filippo and Puglisi, Simon J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14510},
URN = {urn:nbn:de:0030-drops-145100},
doi = {10.4230/LIPIcs.MFCS.2021.70},
annote = {Keywords: Constructive ordinals, Cantor normal forms, Brouwer trees}
}
#20
@article{kraus:inftyCwFs,
author = {Kraus, Nicolai},
title = {Internal Infinity-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT},
year = {2021},
booktitle = {Symposium on Logic in Computer Science (LICS 2021)},
pages = {1-14},
doi = {10.1109/LICS52264.2021.9470667}
}
#19
@article{krausVonRaumer:wellfounded,
author = {Nicolai Kraus and Jakob von Raumer},
title = {Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory},
year = {2020},
isbn = {9781450371049},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3373718.3394800},
doi = {10.1145/3373718.3394800},
booktitle = {Symposium on Logic in Computer Science (LICS 2020)},
pages = {662–675},
keywords = {graph cycle, graph rewriting, coherence, well-founded relation, free group, van Kampen, coequaliser, homotopy type theory, set-quotient, local confluence},
location = {Saarbr\"{u}cken, Germany},
}
#18
@article{annenkov_capriotti_kraus_sattler_2023,
author={Annenkov, Danil and Capriotti, Paolo and Kraus, Nicolai and Sattler, Christian},
title={Two-level type theory and applications},
DOI={10.1017/S0960129523000130},
journal={Mathematical Structures in Computer Science},
publisher={Cambridge University Press},
year={2023},
pages={1-56}
}
#17
@InProceedings{KapKovKra:embedding,
author = {Kaposi, Ambrus and Kov{\'a}cs, Andr{\'a}s and Kraus, Nicolai},
editor = {Hutton, Graham},
title = {Shallow Embedding of Type Theory is Morally Correct},
booktitle = {Mathematics of Program Construction},
year = {2019},
publisher = {Springer International Publishing},
address = {Cham},
pages = {329--365},
isbn = {978-3-030-33636-3}
}
#16
@inproceedings{PinyoKraus:twistedCubes,
author = {Gun Pinyo and Nicolai Kraus},
title = {From Cubes to Twisted Cubes via Graph Morphisms in Type Theory},
year = {2019},
url = {https://arxiv.org/abs/1902.10820},
}
#15
@article{KrausVonRaumer:pathSpaces,
author = {Nicolai Kraus and Jakob von Raumer},
title = {Path Spaces of Higher Inductive Types in Homotopy Type Theory},
booktitle = {Symposium on Logic in Computer Science (LICS 2019)},
year = {2019},
url = {https://arxiv.org/abs/1901.06022},
doi = {10.1109/LICS.2019.8785661},
}
#14
@article{Kraus:free,
title = {Free higher groups in homotopy type theory},
author = {Kraus, Nicolai and Altenkirch, Thorsten},
booktitle = {Symposium on Logic in Computer Science (LICS 2018)},
pages = {599--608},
year = {2018},
organization = {ACM}
}
#13
@inproceedings{ACDKNF,
author = {Thorsten Altenkirch and Paolo Capriotti and Gabe Dijkstra and Nicolai Kraus and Fredrik Nordvall Forsberg},
title = {Quotient inductive-inductive types},
booktitle = {Foundations of Software Science and Computation
Structures (FoSSaCS 2018)},
year = {2018},
doi = {10.1007/978-3-319-89366-2_16},
pages = {293--310},
}
#12
@article{capKra_semisegal,
author = {Paolo Capriotti and Nicolai Kraus},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {POPL'18},
title = {Univalent Higher Categories via Complete Semi-Segal Types},
year = {2017},
month = {dec},
issue_date = {January 2018},
issn = {2475-1421},
pages = {44:1--44:29},
articleno = {44},
numpages = {29},
url = {http://doi.acm.org/10.1145/3158132},
doi = {10.1145/3158132},
acmid = {3158132},
publisher = {ACM},
note = {Full version available at \url{https://arxiv.org/abs/1707.03693}},
}
#11
@article{kraus-sattler:spacediagrams,
author = {Nicolai Kraus and Christian Sattler},
journal = {ArXiv e-prints},
title = {Space-Valued Diagrams, Type-Theoretically (Extended
Abstract)},
year = {2017},
url = {https://arxiv.org/abs/1704.04543v1},
}
#10
@inbook{alt-dan-kra:partiality,
address = {Berlin, Heidelberg},
author = {Altenkirch, Thorsten and Danielsson, Nils Anders and
Kraus, Nicolai},
booktitle = {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,
Uppsala, Sweden, April 22-29, 2017, Proceedings},
editor = {Esparza, Javier and Murawski, Andrzej S.},
pages = {534--549},
publisher = {Springer Berlin Heidelberg},
title = {Partiality, Revisited},
year = {2017},
doi = {10.1007/978-3-662-54458-7_31},
isbn = {978-3-662-54458-7},
url = {http://dx.doi.org/10.1007/978-3-662-54458-7_31},
}
#9
@inproceedings{altCapKra_twoLevels,
address = {Dagstuhl, Germany},
author = {Thorsten Altenkirch and Paolo Capriotti and
Nicolai Kraus},
booktitle = {25th EACSL Annual Conference on Computer Science
Logic (CSL 2016)},
editor = {Jean-Marc Talbot and Laurent Regnier},
pages = {21:1--21:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
title = {Extending Homotopy Type Theory with Strict Equality},
volume = {62},
year = {2016},
annote = {Keywords: homotopy type theory, coherences, strict
equality, homotopy type system},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21},
isbn = {978-3-95977-022-4},
issn = {1868-8969},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/6561},
urn = {urn:nbn:de:0030-drops-65612},
}
#8
@inproceedings{Kraus:2016:CNH:2933575.2933586,
address = {New York, NY, USA},
author = {Kraus, Nicolai},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on
Logic in Computer Science (LiCS'16)},
pages = {595--604},
publisher = {ACM},
title = {Constructions with Non-Recursive Higher Inductive
Types},
year = {2016},
doi = {10.1145/2933575.2933586},
isbn = {978-1-4503-4391-6},
url = {http://doi.acm.org/10.1145/2933575.2933586},
}
#7
@inproceedings{capKraVez_elimTruncs,
address = {Dagstuhl, Germany},
author = {Paolo Capriotti and Nicolai Kraus and Andrea Vezzosi},
booktitle = {24th EACSL Annual Conference on Computer Science
Logic (CSL) 2015)},
editor = {Stephan Kreutzer},
pages = {359--373},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
title = {Functions out of Higher Truncations},
volume = {41},
year = {2015},
annote = {Keywords: homotopy type theory, truncation
elimination, constancy on loop spaces},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2015.359},
isbn = {978-3-939897-90-3},
issn = {1868-8969},
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5425},
urn = {urn:nbn:de:0030-drops-54257},
}
#6
@phdthesis{nicolai:thesis,
address = {Nottingham, UK},
author = {Nicolai Kraus},
school = {School of Computer Science, University of Nottingham},
title = {Truncation Levels in Homotopy Type Theory},
year = {2015},
}
#5
@inproceedings{kraus_generaluniversalproperty,
address = {Dagstuhl, Germany},
author = {Nicolai Kraus},
booktitle = {20th International Conference on Types for Proofs and
Programs (TYPES 2014)},
editor = {Hugo Herbelin and Pierre Letouzey and
Matthieu Sozeau},
pages = {111--145},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
title = {The General Universal Property of the Propositional
Truncation},
volume = {39},
year = {2015},
annote = {Keywords: coherence conditions, propositional
truncation, Reedy limits, universal property,
well-behaved constancy},
doi = {http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.111},
isbn = {978-3-939897-88-0},
issn = {1868-8969},
url = {http://drops.dagstuhl.de/opus/volltexte/2015/5494},
urn = {urn:nbn:de:0030-drops-54944},
}
#4
@article{lmcs:3217,
author = {Kraus, Nicolai and Escard{\'o}, Mart\'{\i}n H. and
Coquand, Thierry and Altenkirch, Thorsten},
journal = {Logical Methods in Computer Science},
month = {mar},
note = {In the special issue of TLCA'13},
title = {Notions of Anonymous Existence in {M}artin-{L}\"of
Type Theory},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/LMCS-13(1:15)2017},
url = {http://lmcs.episciences.org/3217},
}
#3
@article{krausSattler_universes,
author = {Kraus, Nicolai and Sattler, Christian},
journal = {ACM Transactions on Computational Logic (TOCL)},
month = {April},
number = {2},
pages = {18:1--18:12},
publisher = {ACM},
title = {Higher Homotopies in a Hierarchy of Univalent
Universes},
volume = {16},
year = {2015},
}
#2
@inproceedings{krausgeneralizations,
author = {Nicolai Kraus and Mart\'{\i}n H. Escard\'{o} and
Thierry Coquand and Thorsten Altenkirch},
booktitle = {Typed Lambda Calculus and Applications (TLCA)},
editor = {Masahito Hasegawa},
pages = {173--188},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Generalizations of {H}edberg's Theorem},
volume = {7941},
year = {2013},
doi = {10.1007/978-3-642-38946-7_14},
}
#1
@article{Abel:1395187,
author = {Abel, Andreas and Kraus, Nicolai},
journal = {EPTCS 71},
month = {Nov},
note = {Comments: In Proceedings LFMTP 2011, arXiv:1110.6685},
number = {arXiv:1111.0085},
title = {A Lambda Term Representation Inspired by Linear
Ordered Logic},
year = {2011},
doi = {10.4204/EPTCS.71},
url = {http://cds.cern.ch/record/1395187},
}