A Hierarchy for Delimited Continuations in Call-by-Name

Λµ-calculus was introduced as a Böhm-complete extension of Parigot's λµ-calculus. Λµ-calculus, contrarily to Parigot's calculus, is a calculus of CBN delimited control as evidenced by Herbelin and Ghilezan. In their seminal paper on (CBV) delimited control, Danvy and Filinski introduced the CPS Hierarchy of control operators (shifti/reseti)i∈ω. In a similar way, we introduce in the present paper the Stream Hierarchy, a hierarchy of calculi extending and generalizing Λµ-calculus. The (Λn )n∈ω-calculi have Church-Rosser and Böhm theorems. We then present sound and complete CPS translations for the hierarchy which lead to a new CPS translation for Λµ and simpler completeness proofs. Next, we investigate the operational content of the hierarchy through ract machines, the (Λn )n∈ω-KAM. Finally, we establish that the Stream hierarchy is indeed a CBN analogous to the CPS hierarchy.

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: Alexis Saurin
• Keywords: Applied Computing, Cps Hierarchy, Cps Translation, FOSSACS 2010, Stream Hierarchy