| 2026 | CRYPTO | Halfspace Learning for Lattice Signature Key Recovery from Signs. | Marcus Brinkmann, Nicolai Kraus, Alexander May |
| 2026 | LICS | Generalized Decidability via Brouwer Trees. | Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg |
| 2025 | LICS | Ordinal Exponentiation in Homotopy Type Theory. | Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu |
| 2025 | PKC | One Bit to Rule Them All - Imperfect Randomness Harms Lattice Signatures. | Simon Damm, Nicolai Kraus, Alexander May, Julian Nowakowski, Jonas Thietke |
| 2024 | LICS | On symmetries of spheres in univalent foundations. | Pierre Cagne, Ulrik Torben Buchholtz, Nicolai Kraus, Marc Bezem |
| 2023 | LICS | Set-Theoretic and Type-Theoretic Ordinals Coincide. | Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu |
| 2021 | LICS | Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. | Nicolai Kraus |
| 2021 | MFCS | Connecting Constructive Notions of Ordinals in Homotopy Type Theory. | Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu |
| 2020 | LICS | Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. | Nicolai Kraus, Jakob von Raumer |
| 2019 | LICS | Path Spaces of Higher Inductive Types in Homotopy Type Theory. | Nicolai Kraus, Jakob von Raumer |
| 2019 | MPC | Shallow Embedding of Type Theory is Morally Correct. | Ambrus Kaposi, Andrs Kovcs, Nicolai Kraus |
| 2018 | FOSSACS | Quotient Inductive-Inductive Types. | Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg |
| 2018 | LICS | Free Higher Groups in Homotopy Type Theory. | Nicolai Kraus, Thorsten Altenkirch |
| 2017 | FOSSACS | Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type. | Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus |
| 2016 | CSL | Extending Homotopy Type Theory with Strict Equality. | Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus |
| 2016 | LICS | Constructions with Non-Recursive Higher Inductive Types. | Nicolai Kraus |
| 2015 | CSL | Functions out of Higher Truncations. | Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi |