关注
Nicolai Kraus
标题
引用次数
引用次数
年份
Homotopy Type Theory: Univalent Foundations of Mathematics
P Aczel, B Ahrens, T Altenkirch, S Awodey, B Barras, A Bauer, Y Bertot, ...
146*2013
Two-level type theory and applications
D Annenkov, P Capriotti, N Kraus, C Sattler
Mathematical Structures in Computer Science, 1-56, 2023
94*2023
Quotient Inductive-Inductive Types.
T Altenkirch, P Capriotti, G Dijkstra, N Kraus, F Nordvall Forsberg
FoSSaCS, 293-310, 2018
772018
Extending Homotopy Type Theory with Strict Equality
T Altenkirch, P Capriotti, N Kraus
25th EACSL Annual Conference on Computer Science Logic (CSL 2016) 62 (10 …, 2016
632016
Partiality, revisited
T Altenkirch, NA Danielsson, N Kraus
International Conference on Foundations of Software Science and Computation …, 2017
622017
Notions of Anonymous Existence in Martin-Löf Type Theory
N Kraus, M Escardó, T Coquand, T Altenkirch
Logical Methods in Computer Science 13 (1), 2017
43*2017
The general universal property of the propositional truncation
N Kraus
postproceedings of Types for Proofs and Programs (TYPES), 2014
402014
Univalent higher categories via complete semi-segal types
P Capriotti, N Kraus
POPL - Proceedings of the ACM on Programming Languages 2 (POPL), 1-29, 2017
302017
Constructions with non-recursive higher inductive types
N Kraus
ACM/IEEE Symposium on Logic in Computer Science (LICS), 595--604, 2016
292016
Generalizations of Hedberg’s Theorem
N Kraus, M Escardó, T Coquand, T Altenkirch
Typed Lambda Calculi and Applications (TLCA'13) 7941, 173-188, 2013
292013
Truncation levels in homotopy type theory
N Kraus
University of Nottingham, 2015
252015
Higher homotopies in a hierarchy of univalent universes
N Kraus, C Sattler
ACM Transactions on Computational Logic (TOCL) 16 (2), 18, 2015
25*2015
Free higher groups in homotopy type theory
N Kraus, T Altenkirch
LICS '18 Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in …, 2018
212018
Path spaces of higher inductive types in homotopy type theory
N Kraus, J von Raumer
2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2019
202019
Shallow embedding of type theory is morally correct
A Kaposi, A Kovács, N Kraus
International Conference on Mathematics of Program Construction, 329-365, 2019
132019
Internal∞-categorical models of dependent type theory: Towards 2LTT eating HoTT
N Kraus
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-14, 2021
112021
Space-valued diagrams, type-theoretically
N Kraus, C Sattler
arXiv preprint arXiv:1704.04543, 2017
112017
Connecting constructive notions of ordinals in homotopy type theory
N Kraus, FN Forsberg, C Xu
arXiv preprint arXiv:2104.02549, 2021
102021
Coherence via well-foundedness: Taming set-quotients in homotopy type theory
N Kraus, J Von Raumer
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020
10*2020
Set-theoretic and type-theoretic ordinals coincide
T de Jong, N Kraus, FN Forsberg, C Xu
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2023
92023
系统目前无法执行此操作，请稍后再试。
文章 1–20