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.AI2024
Formally Verified Approximate Policy Iteration
Maximilian Schäffeler, Mohammad Abdulaziz
We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the form…