A type-theoretic foundation of delimited continuations

DOI10.1007/s10990-007-9006-0zbMath1213.68187OpenAlexW2128246210MaRDI QIDQ968364

Hugo Herbelin, Zena M. Ariola, Amr Sabry

Publication date: 5 May 2010

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00177326/file/hosc-AriHerSab07-delim-cont.pdf

zbMATH Keywords

promptshiftmonadresetcallccsubtractionsubcontinuation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items

Delimited control operators prove double-negation shift ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Classical Call-by-Need and Duality ⋮ Delimited control and computational effects

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A syntactic theory of sequential control
• The revised report on the syntactic theories of sequential control and state
• A syntactic theory of dynamic binding
• Unchecked exceptions can be strictly more powerful than call/cc
• Comparing control constructs by double-barrelled CPS
• λμ-calculus and Böhm's theorem
• Explicit Substitutions and Reducibility
• The duality of computation
• Control reduction theories: the benefit of structural substitution
• Obtaining coroutines with continuations
• Semi-Boolean algebras and their applications to intuitionistic logic with dual operations
• A Formulae-as-Types Interpretation of Subtractive Logic
• Sound and complete axiomatisations of call-by-value control operators
• A type-theoretic foundation of continuations and prompts
• A sound and complete axiomatization of delimited continuations
• A monadic framework for delimited continuations
• Subtractive logic