Extracting a Call-by-Name Partial Evaluator from a Proof of Termination

It is well known that the computational content of a termination proof of a calculus is an interpreter that computes the result of an input term. Traditionally, such extraction has been tried for a calculus with deterministic reduction rules, producing the result as a value, i.e., in weak head normal form where no redexes are reduced under lambda. In this paper, we consider non-deterministic reduction rules where any redexes can be reduced, even the ones under lambda, and extract a partial evaluator, rather than an interpreter, that produces the result in normal form. We formalize a call-by-name, simply-typed, lambda calculus in the Agda proof assistant and prove its termination using a logical predicate. We observe that the extracted program can be regarded as an online partial evaluator and present future perspectives about how we can extend the framework to a call-by-value calculus.