Pierre Boutillier, Delimited Control and Continuation Passing Style in Pure Type Systems


  • Feb. 16, 2012, 15:30 - 16:15


Pure Type Systems provide with a generic framework at the intersection of proof theory and programming languages for studying arbitrary type systems over the dependent product type. The power of expressivity is made by an appropriate choice of sorts, of axioms for typing sorts and of rules for governing the formation of dependent products.

The syntax of Pure Type Systems mixes terms and types in the same syntactical category. This forbids continuation-passing-style (cps) transformations in their full generality. Therefore, control operators do not behave correctly with dependent types in general. Logically sound restrictions of dependently typed frameworks with control operators have been successfully exhibited by Coquand and Herbelin [3] and by Barthe, Hatcliff and Sørensen [1, 2] by restricting the sorts where control can occur. (It allows the cps transformation only on objects living in types whose sort does not type another sort.)

We propose a new kind of restriction thanks to delimited control. Delimiters provide a way to go out of the cps monad under certain circumstances. We use them each time we need to staunch the calculus. To ensure that the correct circumstances hold, product types are annotated with return types and we use a annotated typing system that comes forward from the cps transformation and follows what Danvy and Filinski[4] made in the simply type lambda-calculus.


[1] Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. A notion of classical pure type system. Electr. Notes Theor. Comput. Sci., 6:4–59, 1997.

[2] Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. Cps translations and applications: The cube and beyond. Higher-Order and Symbolic Computation, 12(2):125–170, 1999.

[3] Thierry Coquand and Hugo Herbelin. A-translation and looping combinators in pure type systems. Journal of Functional Programming, 4(1):77–88, 1994.

[4] Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark, August 1989.