Available in
PostScript and
dvi
formats.
Abstract: We study the continuation passing style
(CPS) transform and its generalization, the computational
transform, in which the notion of computation is generalized from
continuation passing to an arbitrary one. To establish a relation
between direct style and continuation passing style
interpretation of sequential call-by-value programs, we prove the
Retraction Theorem which says that a lambda term can be recovered from
its continuationized form via a lambda-definable retraction. The
Retraction Theorem is proved in the logic of the computational lambda
calculus for the simply typed terms.
Available in
PostScript and
dvi
formats.
Abstract: In this thesis we present two applications
of using types of a typed lambda calculus to derive equation schemas,
instances of which are provable by convertibility.
Part 1: Retraction Approach to CPS Transform. See above.
Part 2: Another Look at ``Theorems for Free!''. We reexamine
Wadler's ``free theorems'' - theorems about polymorphic functions
derivable from the type of the function - in an extension of
Mairson's syntactic treatment of logical relations. Logical relations
are defined as formulas in second (and higher) order logic over
untyped lambda terms, from which we can instantiate equations
involving a given term. As a consequence we can formulate a free
theorem as an equation schema, each instance of which is provable by
convertibility, given typing conditions on the terms involved are met.
In our framework datatypes are represented as free algebras generated
by constants, and we define sufficient conditions which a
representation of a datatype must satisfy to preserve free theorems.
As a special case we prove examples of free theorems, as equations by
convertibility, using Bohm-Berarducci representation of
datatypes.
Available as
technical report from
Lotus
Workgroup Technologies Group.
Abstract: We introduce the Notification Service
Transfer Protocol (NSTP), which provides a simple, common service for
sharing state in synchronous multi-user applications. A Notification
Server provides items of shared state to a collection of clients and
notifies the clients whenever one of the items changes. The division
between client and server in this system is unusual; the centralized
state is uninterpreted by the server. Instead, the responsibility for
semantics and processing falls on the clients, which collude to
implement the application. After describing NSTP, we differentiate it
from other systems in terms of the four design principles that have
guided its development.
Abstract: We present an evaluation technique for
proving strong normalization (SN). We use the technique to give SN
proofs for $F_2$, $F$-bounded quantification, subtypes, and
$F_\omega$. The evaluation technique derives SN as a corollary of the
soundness of the typing rules under an appropriate evaluation
semantics. The evaluation semantics yields simpler type sets than
those used in earlier SN proofs. The type sets discussed here form a
complete lattice under classical union and intersection. The
simplified type sets allow a simplified treatment of a variety of type
constructors.
To find out about my education and work experience look up my curriculum vitae.