Bibliography for Nicolai Kraus
#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 ∞-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},
}