[POPLmark] Type safety via evaluation contexts in Twelf

[Chung-chieh Shan]

As a part of our work on lightweight static capabilities [1] and their
use in assuring safety of array and list accesses, we have formalized in
Twelf the soundness of an extension of System F with lists and non-empty
lists, with small-step operational semantics.  We are writing to seek
comments and suggestions.

We use evaluation contexts in the operational semantics and the safety
and progress proofs, thus closely following the `Syntactic Approach to
Type Soundness'.  This formalization differs only cosmetically from
the well-known Twelf formalizations, and merely sets the stage for the
next message about formalizing dynamic binding.  The use of term->term
functions to model evaluation contexts might be of mild interest.  The
same idea appears in `Mechanizing the Metatheory of Standard ML' [2]
though not in the operational semantics as here.  We'd like therefore to
contribute the commented Twelf code [3].

Indeed, the type preservation and progress proofs factor out into the
type preservation for redexes, and the progress for typed pre-values.
The context typing rules are shared across the preservation and progress
proofs.

	Ken and Oleg

[1] http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html
[2] http://www.cs.cmu.edu/~dklee/tslf/
[3] http://pobox.com/~oleg/ftp/Computation/safety.elf
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20060920/8dfbc3bb/attachment.sig