A type-theoretic foundation of delimited continuations

DOI10.1007/S10990-007-9006-0MaRDI QIDQ968364zbMATH OpenOpenAlexFDO

Authors Zena M. Ariola, Hugo Herbelin, 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

promptmonadresetshiftcallccsubtractionsubcontinuation

Mathematics Subject Classification ID

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

Recommendations

• A type-theoretic foundation of continuations and prompts
• scientific article; zbMATH DE number 1759490
• Subtyping delimited continuations
• A Substructural Type System for Delimited Continuations
• Polymorphic Delimited Continuations

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3972162 (Why is no real title available?)
• scientific article; zbMATH DE number 177780 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 512771 (Why is no real title available?)
• scientific article; zbMATH DE number 2038761 (Why is no real title available?)
• scientific article; zbMATH DE number 1538034 (Why is no real title available?)
• scientific article; zbMATH DE number 1759490 (Why is no real title available?)
• A Formulae-as-Types Interpretation of Subtractive Logic
• A monadic framework for delimited continuations
• A sound and complete axiomatization of delimited continuations
• A syntactic theory of dynamic binding
• A syntactic theory of sequential control
• A type-theoretic foundation of continuations and prompts
• Comparing control constructs by double-barrelled CPS
• Control reduction theories: the benefit of structural substitution
• Explicit substitutions and reducibility
• Obtaining coroutines with continuations
• Semi-Boolean algebras and their applications to intuitionistic logic with dual operations
• Sound and complete axiomatisations of call-by-value control operators
• Subtractive logic
• The duality of computation
• The revised report on the syntactic theories of sequential control and state
• Unchecked exceptions can be strictly more powerful than call/cc
• \(\lambda\mu\)-calculus and Böhm's theorem

Cited in

(22)

• Typed Dynamic Control Operators for Delimited Continuations
• Polymorphic Delimited Continuations
• Hoare-style reasoning with (algebraic) continuations
• A Substructural Type System for Delimited Continuations
• On typing delimited continuations: Three new solutions to the printf problem
• scientific article; zbMATH DE number 7269245 (Why is no real title available?)
• Axiomatizing subtyped delimited continuations
• A monadic framework for delimited continuations
• A Formulae-as-Types Interpretation of Subtractive Logic
• A type-theoretic foundation of continuations and prompts
• Control effects as a modality
• Delimited control operators prove double-negation shift
• A classical sequent calculus with dependent types
• A type system for continuation calculus
• Compositional semantics for composable continuations: from abortive to delimited control
• Classical call-by-need and duality
• Implementing first-class polymorphic delimited continuations by a type-directed selective CPS-transform
• Declarative continuations: an investigation of duality in programming language semantics
• scientific article; zbMATH DE number 1759490 (Why is no real title available?)
• Subtyping delimited continuations
• Delimited control and computational effects
• A sound and complete axiomatization of delimited continuations

This page was built for publication: A type-theoretic foundation of delimited continuations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q968364)