[POPLmark] Type safety via evaluation contexts in Twelf
ccshan at cs.rutgers.edu
Wed Sep 20 14:35:52 EDT 2006
As a part of our work on lightweight static capabilities  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' 
though not in the operational semantics as here. We'd like therefore to
contribute the commented Twelf code .
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
Ken and Oleg
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 189 bytes
Desc: Digital signature
Url : http://lists.seas.upenn.edu/pipermail/poplmark/attachments/20060920/8dfbc3bb/attachment.sig
More information about the Poplmark