Bibliography for Nicolai Kraus




#15
@inproceedings{Kraus:free,
  author =        {Nicolai Kraus and Thorsten Altenkirch},
  title =         {Free Higher Groups in Homotopy Type Theory},
  year =          {2018},
  doi =           {10.1145/3209108.3209183},
  note =          {To appear at LiCS'18},
}



#14
@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},
}



#13
@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}},
}



#12
@article{ann-cap-kra:two-level,
  author =        {Danil Annenkov and Paolo Capriotti and Nicolai Kraus},
  journal =       {ArXiv e-prints},
  month =         {may},
  title =         {Two-Level Type Theory and Applications},
  year =          {2017},
  url =           {http://arxiv.org/abs/1705.03307},
}



#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},
}



#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},
}