A Lambda Term Representation Inspired by Linear Ordered Logic - Andreas Abel 001; Nicolai Kraus (LFMTP, 2011)

Generalizations of Hedberg's Theorem. - Nicolai Kraus; Martín Hötzel Escardó; Thierry Coquand; Thorsten Altenkirch (TLCA, 2013)

On the Hierarchy of Univalent Universes: U(n) is not n-Truncated. - Nicolai Kraus; Christian Sattler (CoRR, 2013)

The General Universal Property of the Propositional Truncation. - Nicolai Kraus (TYPES, 2014)

Functions out of Higher Truncations. - Paolo Capriotti; Nicolai Kraus; Andrea Vezzosi (CSL, 2015)

Higher Homotopies in a Hierarchy of Univalent Universes. - Nicolai Kraus; Christian Sattler (ACM Trans. Comput. Log., 2015)

Truncation levels in homotopy type theory. - Nicolai Kraus (2015)

Extending Homotopy Type Theory with Strict Equality. - Thorsten Altenkirch; Paolo Capriotti; Nicolai Kraus (CSL, 2016)

Constructions with Non-Recursive Higher Inductive Types. - Nicolai Kraus (LICS, 2016)

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. - Thorsten Altenkirch; Nils Anders Danielsson; Nicolai Kraus (FoSSaCS, 2017)

Two-Level Type Theory and Applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus (CoRR, 2017)

Notions of Anonymous Existence in Martin-Löf Type Theory. - Nicolai Kraus; Martín Escardó; Thierry Coquand; Thorsten Altenkirch (Log. Methods Comput. Sci., 2017)

Space-Valued Diagrams, Type-Theoretically (Extended Abstract). - Nicolai Kraus; Christian Sattler (CoRR, 2017)

Quotient Inductive-Inductive Types. - Thorsten Altenkirch; Paolo Capriotti; Gabe Dijkstra; Nicolai Kraus; Fredrik Nordvall Forsberg (FoSSaCS, 2018)

Free Higher Groups in Homotopy Type Theory. - Nicolai Kraus; Thorsten Altenkirch (LICS, 2018)

Univalent higher categories via complete Semi-Segal types. - Paolo Capriotti; Nicolai Kraus (Proc. ACM Program. Lang., 2018)

Path Spaces of Higher Inductive Types in Homotopy Type Theory. - Nicolai Kraus; Jakob von Raumer (LICS, 2019)

Shallow Embedding of Type Theory is Morally Correct. - Ambrus Kaposi; András Kovács; Nicolai Kraus (MPC, 2019)

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. - Gun Pinyo; Nicolai Kraus (TYPES, 2019)

Control of KNX devices over IEEE 11073 service-oriented device connectivity. - Nicolai Kraus; Marc Viertel; Oliver Burgert (ICPS, 2020)

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. - Nicolai Kraus; Jakob von Raumer (LICS, 2020)

Coherence via Wellfoundedness. - Nicolai Kraus; Jakob von Raumer (CoRR, 2020)

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. - Nicolai Kraus (LICS, 2021)

Connecting Constructive Notions of Ordinals in Homotopy Type Theory. - Nicolai Kraus; Fredrik Nordvall Forsberg; Chuangjie Xu (MFCS, 2021)

A rewriting coherence theorem with applications in homotopy type theory. - Nicolai Kraus; Jakob von Raumer (Math. Struct. Comput. Sci., 2022)

Set-Theoretic and Type-Theoretic Ordinals Coincide. - Tom de Jong; Nicolai Kraus; Fredrik Nordvall Forsberg; Chuangjie Xu (LICS, 2023)

Two-level type theory and applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2023)

Type-theoretic approaches to ordinals. - Nicolai Kraus; Fredrik Nordvall Forsberg; Chuangjie Xu (Theor. Comput. Sci., 2023)

On symmetries of spheres in univalent foundations. - Pierre Cagne; Ulrik Torben Buchholtz; Nicolai Kraus; Marc Bezem (LICS, 2024)

Two-level type theory and applications - ERRATUM. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2024)

TIBA: A web application for the visual analysis of temporal occurrences, interactions, and transitions of animal behavior. - Nicolai Kraus; Michael Aichem; Karsten Klein 001; Etienne Lein; Alex Jordan; Falk Schreiber (PLoS Comput. Biol., 2024)

One Bit to Rule Them All - Imperfect Randomness Harms Lattice Signatures. - Simon Damm; Nicolai Kraus; Alexander May 001; Julian Nowakowski; Jonas Thietke (IACR Cryptol. ePrint Arch., 2025)

Ordinal Exponentiation in Homotopy Type Theory. - Tom de Jong; Nicolai Kraus; Fredrik Nordvall Forsberg; Chuangjie Xu (CoRR, 2025)