[POPLmark] Mechanising dynamic binding

[Chung-chieh Shan]

We suggest that POPLmark include challenge problems for control effects,
where the result of an expression depends on its evaluation context.  As
a concrete instance, we demonstrate mechanising mutable dynamic binding
in a direct-style semantics, without environment- or state-passing but
relying instead on the evaluation context to play the prominent double
role of the dynamic environment.  Again we write to seek comments and
suggestions.

Following Moreau (HOSC 1998), we call a *dynamic variable* a variable
whose association with a value exists only within the dynamic
extent of an expression, that is, while control remains within that
expression.  If several associations exist for the same variable at
the same time, the latest one takes effect.  Such association is
called a *dynamic binding*.  Examples of dynamic variables include
exception handlers, stdin, and hostname (for mobile code).  Given this
abstract specification, dynamic binding can be implemented in many
ways: by adding an environment argument to each function (so-called
environment-passing style), using global mutable cells (shallow
binding), and so on.

Moreau developed such an abstract, syntactic theory of dynamic binding.
We add a sound type system [1].  Our formalization of type safety uses
the reduction semantics published by Moreau as Figure 6.  Our type
system is conventional, except that judgements are parameterised by a
signature Sigma, which associates every dynamic variable with its type.
This type system does not prevent access to an unbound dynamic variable,
which matches the existing practice.

Our Twelf code [2] closely follows the small-step approach of `Syntactic
Approach to Type Soundness' with contexts, focusing and redexing.
Evaluation contexts are modeled as meta-level functions.  The notable
complication is that contexts and pre-values are mutually dependent,
and so the pre-val and focus functions are mutually recursive.  Another
complication is that our type system specifically lets a well-typed
expression try to access an unbound dynamic variable, resulting in an
error.  This reflects the behavior of most real systems that use dynamic
variables.  We have to model this error behavior and account for it in
our progress proofs.

We plan to mechanise the rest of our paper [1]: delimited control and a
type-preserving translation from dynamic binding to delimited control.

	Oleg and Ken

[1] http://pobox.com/~oleg/ftp/papers/DDBinding.pdf
    Figure 1, Section 2, and Section 6.1
[2] http://pobox.com/~oleg/ftp/Computation/db-lang.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/6dc20472/attachment.sig