A Typed Context Calculus

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Masatomo Hashimoto and I have written a paper "A Typed Context Calculus".
We thought some of you might be interested in this. The paper is
available from
or from one of our home pages:
Any comments or suggestions are welcome. The abstract of the paper
				 Atsushi Ohori


This paper develops a typed calculus for contexts i.e., lambda terms
with ``holes.''  In addition to ordinary lambda terms, the calculus
contains {\em labeled holes\/}, {\em hole abstraction\/} and {\em
context application\/} for manipulating first-class contexts. The
primary operation for contexts is {\em hole filling\/} which captures
free variables.  This operation conflicts with the capture-avoiding
substitution of the lambda calculus, and a straightforward mixture of
the two results in an inconsistent system.  We solve this problem by
defining a type system that precisely specifies variable-capturing
properties of contexts as well as their types, and systematically
performing bound variable renaming.  This enables us to define a
reduction system that properly integrates {\em full\/}
$\beta$-reduction and {\em fill\/}-reduction. For this calculus, we
prove the subject reduction property and Church-Rosser property.  This
context calculus will serve a basis for developing programming
languages with advanced features that call for manipulation of open
terms such as flexible first-class modules.