A proof-theoretic foundation of abortive continuations

DOI10.1007/s10990-007-9007-zzbMath1128.68089OpenAlexW2032124026MaRDI QIDQ2464725

Hugo Herbelin, Amr Sabry, Zena M. Ariola

Publication date: 17 December 2007

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

Full work available at URL: https://doi.org/10.1007/s10990-007-9007-z

zbMATH Keywords

Classical logicIntuitionistic logicMinimal logicCallcc

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)

Related Items

Postponement of $\mathsf {raa}$ and Glivenko's theorem, revisited ⋮ Unnamed Item ⋮ Control reduction theories: the benefit of structural substitution ⋮ Adding Negation to Lambda Mu ⋮ Verificationism and Classical Realizability ⋮ A proof-theoretic foundation of abortive continuations ⋮ Classical Call-by-Need and Duality ⋮ Unnamed Item ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Unnamed Item

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The revised report on the syntactic theories of sequential control and state
• Computer science logic. 10th international workshop, CSL '96. Annual conference of the EACSL, Utrecht, the Netherlands. September 21--27, 1996. Selected papers
• Proof theory and automated deduction
• A proof-theoretic foundation of abortive continuations
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Natural 3-valued logics—characterization and proof theory
• A new constructive logic: classic logic
• An environment machine for the λμ-calculus
• Classical logic, continuation semantics and abstract machines
• Proofs of strong normalisation for second order classical natural deduction
• Sound and complete axiomatisations of call-by-value control operators
• A confluent λ-calculus with a catch/throw mechanism
• A type-theoretic foundation of continuations and prompts
• A sound and complete axiomatization of delimited continuations