Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (APLAS, 2023)

The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (CSL, 2024)

Destabilizing Iris. - Simon Spies; Niklas Mück; Haoyi Zeng; Michael Sammler; Andrea Lattuada 001; Peter Müller 001; Derek Dreyer (Proc. ACM Program. Lang., 2025)