Nicolai Kraus

ORCID

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 35

Top Venues

CoRR

LICS

Math. Struct. Comput. Sci.

FoSSaCS

University of Nottingham, UK (PHD)

Education History

University of Nottingham, UK

PHD

Publications

Pierre Cagne, Ulrik Torben Buchholtz, Nicolai Kraus, Marc Bezem
On symmetries of spheres in univalent foundations. LICS (2024)
Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler
Two-level type theory and applications - ERRATUM. Math. Struct. Comput. Sci. 34 (1) (2024)
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus, Marc Bezem
On symmetries of spheres in univalent foundations. CoRR (2024)
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Set-Theoretic and Type-Theoretic Ordinals Coincide. CoRR (2023)
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Type-theoretic approaches to ordinals. Theor. Comput. Sci. 957 (2023)
Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler
Two-level type theory and applications. Math. Struct. Comput. Sci. 33 (8) (2023)
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Set-Theoretic and Type-Theoretic Ordinals Coincide. LICS (2023)
Nicolai Kraus, Jakob von Raumer
A rewriting coherence theorem with applications in homotopy type theory. Math. Struct. Comput. Sci. 32 (7) (2022)
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Type-Theoretic Approaches to Ordinals. CoRR (2022)
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Connecting Constructive Notions of Ordinals in Homotopy Type Theory. MFCS (2021)
Nicolai Kraus
Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. LICS (2021)
Nicolai Kraus, Jakob von Raumer
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory. CoRR (2021)
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
Connecting Constructive Notions of Ordinals in Homotopy Type Theory. CoRR (2021)
Nicolai Kraus
Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT. CoRR (2020)
Nicolai Kraus, Jakob von Raumer
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. LICS (2020)
Nicolai Kraus, Jakob von Raumer
Coherence via Wellfoundedness. CoRR (2020)
Nicolai Kraus, Marc Viertel, Oliver Burgert
Control of KNX devices over IEEE 11073 service-oriented device connectivity. ICPS (2020)
Ambrus Kaposi, András Kovács, Nicolai Kraus
Shallow Embedding of Type Theory is Morally Correct. CoRR (2019)
Gun Pinyo, Nicolai Kraus
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. CoRR (2019)
Nicolai Kraus, Jakob von Raumer
Path Spaces of Higher Inductive Types in Homotopy Type Theory. CoRR (2019)
Ambrus Kaposi, András Kovács, Nicolai Kraus
Shallow Embedding of Type Theory is Morally Correct. MPC (2019)
Nicolai Kraus, Jakob von Raumer
Path Spaces of Higher Inductive Types in Homotopy Type Theory. LICS (2019)
Gun Pinyo, Nicolai Kraus
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. TYPES (2019)
Nicolai Kraus, Thorsten Altenkirch
Free Higher Groups in Homotopy Type Theory. LICS (2018)
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg
Quotient Inductive-Inductive Types. FoSSaCS (2018)
Nicolai Kraus, Thorsten Altenkirch
Free Higher Groups in Homotopy Type Theory. CoRR (2018)
Paolo Capriotti, Nicolai Kraus
Univalent higher categories via complete Semi-Segal types. Proc. ACM Program. Lang. 2 (POPL) (2018)
Nicolai Kraus, Christian Sattler
Space-Valued Diagrams, Type-Theoretically (Extended Abstract). CoRR (2017)
Danil Annenkov, Paolo Capriotti, Nicolai Kraus
Two-Level Type Theory and Applications. CoRR (2017)
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. FoSSaCS (2017)
Nicolai Kraus, Martín Escardó, Thierry Coquand, Thorsten Altenkirch
Notions of Anonymous Existence in Martin-Löf Type Theory. Log. Methods Comput. Sci. 13 (1) (2017)
Nicolai Kraus
Constructions with Non-Recursive Higher Inductive Types. LICS (2016)
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Extending Homotopy Type Theory with Strict Equality. CSL (2016)
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
Extending Homotopy Type Theory with Strict Equality. CoRR (2016)
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type. CoRR (2016)
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
Functions out of Higher Truncations. CoRR (2015)
Nicolai Kraus, Christian Sattler
Higher Homotopies in a Hierarchy of Univalent Universes. ACM Trans. Comput. Log. 16 (2) (2015)
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
Functions out of Higher Truncations. CSL (2015)
Nicolai Kraus
The General Universal Property of the Propositional Truncation. TYPES (2014)
Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch
Generalizations of Hedberg's Theorem. TLCA (2013)
Nicolai Kraus, Christian Sattler
On the Hierarchy of Univalent Universes: U(n) is not n-Truncated. CoRR (2013)
Andreas Abel, Nicolai Kraus
A Lambda Term Representation Inspired by Linear Ordered Logic LFMTP (2011)

Nicolai Kraus.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Nicolai Kraus