2 papers
cs.PL2026
Multi-language Program Logics
Alexander Loitzl, Niklas Mück, Michael Sammler
Real-world programs are rarely written in a single language: For example, C programs call assembly routines, and high-level languages like OCaml link with low-level C libraries. Ye…
cs.LO2023
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions
Yannick Forster, Dominik Kirst, Niklas Mück
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof…