2 papers
cs.LO2025
Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
Kevin Kappelmann, Fabian Huch, Lukas Stevens +1
We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that…
cs.LO2024
Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
Fabian Huch
Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platf…