Nicolai Kraus

According to our database, Nicolai Kraus authored at least 30 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Two-level type theory and applications - ERRATUM.

Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler

Math. Struct. Comput. Sci., 2024

On symmetries of spheres in univalent foundations.

Pierre Cagne, Ulrik Torben Buchholtz, Nicolai Kraus, Marc Bezem

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

2023

Type-theoretic approaches to ordinals.

Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

Theor. Comput. Sci., May, 2023

Two-level type theory and applications.

Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler

Math. Struct. Comput. Sci., 2023

Set-Theoretic and Type-Theoretic Ordinals Coincide.

Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

Proceedings of the 38th Annual ACM/IEEE Symposium on Logic in Computer Science, 2023

2022

A rewriting coherence theorem with applications in homotopy type theory.

Nicolai Kraus, Jakob von Raumer

Math. Struct. Comput. Sci., August, 2022

2021

Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu

Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, 2021

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT.

Nicolai Kraus

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Coherence via Wellfoundedness.

Nicolai Kraus, Jakob von Raumer

CoRR, 2020

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory.

Nicolai Kraus, Jakob von Raumer

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Control of KNX devices over IEEE 11073 service-oriented device connectivity.

Nicolai Kraus, Marc Viertel, Oliver Burgert

Proceedings of the IEEE Conference on Industrial Cyberphysical Systems, 2020

2019

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory.

Gun Pinyo, Nicolai Kraus

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

Shallow Embedding of Type Theory is Morally Correct.

Ambrus Kaposi, András Kovács, Nicolai Kraus

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Path Spaces of Higher Inductive Types in Homotopy Type Theory.

Nicolai Kraus, Jakob von Raumer

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

2018

Univalent higher categories via complete Semi-Segal types.

Paolo Capriotti, Nicolai Kraus

Proc. ACM Program. Lang., 2018

Free Higher Groups in Homotopy Type Theory.

Nicolai Kraus, Thorsten Altenkirch

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Quotient Inductive-Inductive Types.

Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg

Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017

Space-Valued Diagrams, Type-Theoretically (Extended Abstract).

Nicolai Kraus, Christian Sattler

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

Two-Level Type Theory and Applications.

Danil Annenkov, Paolo Capriotti, Nicolai Kraus

CoRR, 2017

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.

Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus

Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016

Constructions with Non-Recursive Higher Inductive Types.

Nicolai Kraus

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Extending Homotopy Type Theory with Strict Equality.

Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Truncation levels in homotopy type theory.

Nicolai Kraus

PhD thesis, 2015

Higher Homotopies in a Hierarchy of Univalent Universes.

Nicolai Kraus, Christian Sattler

ACM Trans. Comput. Log., 2015

Functions out of Higher Truncations.

Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

The General Universal Property of the Propositional Truncation.

Nicolai Kraus

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

2013

On the Hierarchy of Univalent Universes: U(n) is not n-Truncated.

Nicolai Kraus, Christian Sattler

CoRR, 2013

Generalizations of Hedberg's Theorem.

Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2011

A Lambda Term Representation Inspired by Linear Ordered Logic

Andreas Abel, Nicolai Kraus

Proceedings of the Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2011