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

[Dan Licata]

Hi Oleg,

The representation technique you're describing is referred to as
"intrinsic encodings" on the Twelf Wiki:

http://twelf.plparty.org/wiki/Intrinsic_encoding

The idea with the terminology is that "intrinsic encodings" bake
invariants (e.g. well-typedness, valuehood) in using dependent types,
whereas "extrinsic encodings" use separate, after-the-fact judgements to
identify those raw objects that satisfy an invariant.

You can find a simple example of an evaluator on intrinsically typed
syntax (whose type guarantees type preservation, and whose totality
Twelf proves automatically, like in your development) in the code for
"Class 1" of our Oregon Summer School course:

http://twelf.plparty.org/wiki/Summer_school_2008

and see the accompanying slides for some discussion.

One question: Could you elaborate on what you mean by "tagless" in this
context?

-Dan

> 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