Pierre Boutillier, Delimited Control and Continuation Passing Style in Pure Type Systems
Schedule
- Feb. 16, 2012, 15:30 - 16:15
Abstract
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.
References
[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.
Attachments
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.
References
[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.