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

[oleg@okmij.org]

We present two very different mechanized proofs of soundness of a
type-and-effect system for delimited control operators
shift/reset. Our calculus is call-by-value simply-typed
lambda-calculus with constants and answer-type-modifying delimited
control. The dynamic semantics is small-step. This is the calculus
originally proposed by Danvy and Filinski, enhanced by Asai and
Kameyama (APLAS07) with let-bound polymorphism. The constants of the
calculus may include natural numbers, arithmetic, and the
fixpoint. The type of a general expression specifies not only the type
of the produced value but also the _effect_ of the expression. In the
simplest case, the effect may be raising of an exception; more complex
effects include co-routine invocations or backtracking.  The type of a
functional value is not just a->b but rather a/t1->b/t2, so to
describe effects that may occur when the function is applied. Despite
the more complex expression and arrow types, all types are inferred
and no type annotations are required. This is joint work with Kenichi
Asai, Noriko Hirota, Yukiyoshi Kameyama and Chung-chieh Shan.


One mechanized soundness proof is done in Coq with a locally nameless
methodology. The calculus includes the let-bound polymorphism but
omits, for simplicity, the fixpoint and constants.  This development
deals only with meta-theory: it proves subject reduction and progress
properties, but does not infer types and does not evaluate
expressions. The complete Coq development is available at
	http://okmij.org/ftp/formalizations/shift-Coq/README.dr

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.