<div dir="ltr">Thanks, Oleg! I agree that renaming "progress" to "eval" corresponds to the same insight, though expressed differently: instead of observing that progress and preservation give you evaluation, you are observing that evaluation gives you progress! Were any of the items listed on your page published (elsewhere than on the page itself)? Cheers, -- P</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div><div>Too brief? Here's why: <a href="http://www.emailcharter.org/" target="_blank">http://www.emailcharter.org/</a></div></div></div></div></div></div>
<br><div class="gmail_quote">On 18 July 2018 at 11:03, Oleg <span dir="ltr"><<a href="mailto:oleg@okmij.org" target="_blank">oleg@okmij.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
Phil Wadler wrote:<br>
> Progress + Preservation = Evaluation.<br>
> From a constructive proof of progress and preservation, we can assemble a<br>
> constructive evaluator which, for any given number n, will either reduce<br>
> the term to a value (in less than n steps) or show that after n steps of<br>
> reduction the term is not a value. [The key word here is *constructive*.<br>
> Once one has proved progress and preservation constructively, one has<br>
> implemented a constructive evaluator for terms.]<br>
<br>
</span><span class="">> Indeed, in every presentation I can recall the act of proving progress and<br>
> preservation is separated from the act of writing code that can evaluate a<br>
> term, even though the former trivially implies the latter. <br>
<br>
</span>Sorry for being late to the party...<br>
<br>
I can cite quite a few cases where to prove progress and<br>
preservation, one first implements an evaluator -- and the type<br>
soundness comes as a `side-effect' of writing it.  To wit: one writes<br>
an evaluator of the signature (in Twelf terms)<br>
             eval : {E:exp T} non-value E  -> exp T -> type.<br>
The signature expresses subject reduction (preservation) property.<br>
Thus it becomes impossible to write cases of eval that do not<br>
have subject reduction -- the typechecker will complain otherwise. Once we<br>
have finished writing all cases of eval (which can then be used immediately<br>
to evaluate terms) we can ask Twelf if `eval' is total. If Twelf agrees,<br>
we get the proof of progress. This is often called `intrinsic<br>
encoding' of DSLs and has been quite popular in Twelf community. <br>
<br>
The following web page from about 10 years ago<br>
<br>
        <a href="http://okmij.org/ftp/formalizations/index.html#intrinsic" rel="noreferrer" target="_blank">http://okmij.org/ftp/<wbr>formalizations/index.html#<wbr>intrinsic</a><br>
<br>
summarizes this techniques and provides the references I could find. It<br>
also shows several less-trivial progress-preservation proofs done in<br>
this style, in particular, calculus with both staging and delimited<br>
control. The eval function was indeed used in practice, to evaluate<br>
sample terms (and run all the examples that are mentioned in our<br>
papers about that calculus). <br>
<br>
The technique is closely related to `tagless-final', as mentioned on<br>
that web page. Writing a tagless-final evaluator indeed includes<br>
essentially proving subject reduction in the process (even if one<br>
actually is interested in running programs rather than doing proofs).<br>
<br>
<br>
</blockquote></div><br></div>