[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Phil Wadler wrote: > Progress + Preservation = Evaluation. > From a constructive proof of progress and preservation, we can assemble a > constructive evaluator which, for any given number n, will either reduce > the term to a value (in less than n steps) or show that after n steps of > reduction the term is not a value. [The key word here is *constructive*. > Once one has proved progress and preservation constructively, one has > implemented a constructive evaluator for terms.] > Indeed, in every presentation I can recall the act of proving progress and > preservation is separated from the act of writing code that can evaluate a > term, even though the former trivially implies the latter. Sorry for being late to the party... I can cite quite a few cases where to prove progress and preservation, one first implements an evaluator -- and the type soundness comes as a `side-effect' of writing it. To wit: one writes an evaluator of the signature (in Twelf terms) eval : {E:exp T} non-value E -> exp T -> type. The signature expresses subject reduction (preservation) property. Thus it becomes impossible to write cases of eval that do not have subject reduction -- the typechecker will complain otherwise. Once we have finished writing all cases of eval (which can then be used immediately to evaluate terms) we can ask Twelf if `eval' is total. If Twelf agrees, we get the proof of progress. This is often called `intrinsic encoding' of DSLs and has been quite popular in Twelf community. The following web page from about 10 years ago http://okmij.org/ftp/formalizations/index.html#intrinsic summarizes this techniques and provides the references I could find. It also shows several less-trivial progress-preservation proofs done in this style, in particular, calculus with both staging and delimited control. The eval function was indeed used in practice, to evaluate sample terms (and run all the examples that are mentioned in our papers about that calculus). The technique is closely related to `tagless-final', as mentioned on that web page. Writing a tagless-final evaluator indeed includes essentially proving subject reduction in the process (even if one actually is interested in running programs rather than doing proofs).