[TYPES] First mechanized proofs of type soundness of delimited control

[Tom Murphy]

This way of giving the semantics in Twelf isn't new (though it's a lovely way 
to do it, in my opinion). I think it has been independently discovered a couple 
of times. I use it in my thesis, for example 
(http://tom7.org/papers/modal-types-for-mobile-code.pdf, section 4.4.1) and in 
some code on the Twelf wiki. It does scale up to pretty big stuff, in my case 
some typed compilation transformations like CPS and closure conversion. I 
wanted to point out two ways you can take the idea further:

  1. If you syntactically distinguish expressions and values, then the proofs 
become even more beautiful. This is basically just a matter of taking a 
judgment like is-value and internalizing it syntactically, just as you've taken 
a standard well-typedness judgment and internalized it
into the LF types of your expression language. (For a call-by-value language 
you have lam : (val A -> exp B) -> val (A => B) and an inclusion
of values as expressions like value : val A -> exp A and everything follows 
from there.) You can see then that big-step evaluation always results in a 
value, and you get the preservation theorem for free without any additional 
conditions. It just looks like:

eval : exp A -> val A -> type.
%mode eval +E -V.

  2. One trouble with this way of doing it (really the trouble is getting 
spoiled because everything else is so automatic) is that if your big-step 
evaluation relation does not always terminate, then you cannot use stock Twelf 
to automatically prove a kind of progress theorem. Lots of real-sized languages 
are non-terminating, so that's too bad. In my thesis work I modified Twelf to 
add a %partial keyword. It is the same as %total
but it suppresses the termination check. (This differs from %covers in
that it performs output coverage checking, output freeness checking, and 
ensures that if the relation appeals to others, then those others
are either total or partial.) With it, what you're checking is that the
evaluation relation, cast as a logic program, will always be able to make
progress using Twelf's operational semantics (which itself has progress and 
preservation properties). This is a nice way to do the argument that
would be coinductive on paper, although its correspondence with a paper 
argument is not at all simple, formally speaking.

  - Tom

> We have also mechanized type soundness in Twelf, using an approach
> that is different from known to us ways of mechanizing meta-theory in
> Twelf. We present not only progress and subject reduction proofs but
> also the type inferencer and the evaluator: we can run sample terms
> and see their types. Our code includes the standard shift/reset test
> suite. It is Twelf itself that infers and checks object language
> types. We did not specify the type-checking relation since terms not
> typeable in the object language cannot be built. More remarkably, the
> one-step evaluator of our calculus is also the proof term of type
> soundness. In other words, the very _proof_ of type soundness can be
> used to evaluate sample expressions. Proofs literally have a practical
> use.
> 
> The functional relation eval for one-step reduction is defined as
>
>        eval : {E:exp T} non-value E  -> exp T -> type.
> 
> That definition itself is the statement of subject reduction: any
> expression E of type T which is not a value is reduced to an
> expression of the same type T. Furthermore, eval is total: _every_
> non-value can be further reduced. This is the statement of
> progress. We supply the totality declaration, and Twelf agrees.
> 
> The Twelf development is available at
> 	http://okmij.org/ftp/formalizations/tagless-dl.elf
> 
> Here is an introduction to the tagless typed approach to mechanizing
> type soundness in Twelf, for simply typed lambda-calculus:
> 	http://okmij.org/ftp/formalizations/tagless-l.elf
> 
> We have also tried Isabelle/HOL. Without the nominal package, Kenichi
> Asai has formalized Danvy/Filinski calculus with the type-and-effect
> system, without let-polymorphism. He has proved subject reduction.
>    http://okmij.org/ftp/formalizations/shift-Isabelle/README.dr
> To introduce let-polymorphism into this framework, one has to consider
> alpha-renaming more seriously.  He tried Nominal Isabelle for this
> purpose, but without success, because of the eigen variable problem in
> a proof tree.  The bound variables in terms are nicely treated by the
> nominal package, but a similar problem occurred for a variable that is
> introduced within a proof tree that has to be fresh.
> 
> 
>

-- 

[ NEW! : http://tom7.org/       ]
[ OLD! : http://fonts.tom7.com/ ]