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…