[Prev][Next][Index][Thread]
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
ftp://ftp.kurims.kyoto-u.ac.jp/pub/paper/member/ohori/ContextCalc.{dvi,ps}
or from one of our home pages:
http://www.kurims.kyoto-u.ac.jp/~ohori/
http://wwwfun.kurims.kyoto-u.ac.jp/~masatomo/
Any comments or suggestions are welcome. The abstract of the paper
below.
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.