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
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
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.