Title: CPS Translations and Applications: The Cube and Beyond
Authors: Gilles Barthe, John Hatcliff, Morten Heine Soerensen
Source: Higher-order and Symbolic Computation
Continuation passing style (CPS) translations of typed
lambda-calculi have numerous applications. However, the range of
these applications has been confined by the fact that CPS translations
are known for non-dependent type systems only, thus excluding
well-known systems like the calculus of constructions (CC) and the
logical frameworks (LF). This paper presents techniques for CPS
translating systems with dependent types, with an emphasis on pure
type-theoretical applications.
In the first part of the paper we review several lines of work in
which the need for CPS translations of dependent type systems has
arisen, and discuss the difficulties involved with CPS translating
such systems. One way of overcoming these difficulties is to work with
so-called domain-free type systems. Thus, instead of Barendregt's
lambda-cube we shall consider the domain-free lambda-cube, and instead
of traditional pure type systems, we shall consider domain-free pure
type systems.
We therefore begin the second part by reviewing the domain-free
lambda-cube, which includes domain-free versions of CC and LF, and
then present CPS translations for all the systems of the domain-free
lambda-cube. We also introduce Direct Style (DS) (i.e., inverse CPS)
translations for all the systems of the domain-free lambda-cube; such
DS translations, which have been used in a number of applications,
were previously formulated for untyped and simply-typed languages
only.
In the third part we review domain-free pure type
systems and generalize the CPS translations of the domain-free
lambda-cube to a large class of domain-free pure type systems
which includes most of the systems that appear in the literature,
including those of the domain-free lambda-cube. Many translations
that appear in the literature arise as special cases of ours.
In the fourth part of the paper we present two approaches to CPS
translations of traditional pure type systems. The first, indirect,
technique lifts the CPS translation of domain-free pure type systems
to the analogous class of traditional pure type systems by using
results that relate derivations in domain-free and traditional pure
type systems. The second, direct, approach translates derivations,
requiring a certain order on derivations to be well-founded. Both
techniques yield translations for most of the systems that appear in
the literature, including those of Barendregt's lambda-cube.