Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
Logic in Computer Science
2025-04-22 v2
Abstract
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 can simulate (and be simulated by) Turing Machines with a quadratic time and constant space blow-up. Our framework derives while-programs from functional programs written in a subset of Isabelle/HOL, namely tail-recursive functions with first-order arguments and algebraic datatypes. As far as we are aware, it is the first framework targeting a computation model that is reasonable in time and space from a complexity-theoretic perspective.
Cite
@article{arxiv.2503.02975,
title = {Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model},
author = {Kevin Kappelmann and Fabian Huch and Lukas Stevens and Mohammad Abdulaziz},
journal= {arXiv preprint arXiv:2503.02975},
year = {2025}
}