A Formulae-as-Types Interpretation of Subtractive Logic

DOI10.1093/LOGCOM/14.4.529MaRDI QIDQ4823807zbMATH OpenOpenAlexFDO

Authors T. Crolard

Publication date 28 October 2004

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/5c4363af97178d0ed468b6dc83b377a4f874fde6

zbMATH Keywords

Curry-Howard isomorphismcontrol operatorscoroutinessubtractive logic

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1222571
• Subtractive logic
• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• A type-theoretic foundation of delimited continuations
• A proof-theoretic foundation of abortive continuations

Cited in

(15)

• Intuitionistic Letcc via Labelled Deduction
• Subtractive logic
• Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
• A connection-based characterization of bi-intuitionistic validity
• Dualized simple type theory
• A connection-based characterization of bi-intuitionistic validity
• Pragmatic and dialogic interpretations of bi-intuitionism. I
• Classical Logic with Mendler Induction
• A type-theoretic foundation of delimited continuations
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Deep Inference in Bi-intuitionistic Logic
• Hennessy-Milner properties via topological compactness
• The semi Heyting-Brouwer logic
• On the computational representation of classical logical connectives
• Natural deduction for bi-intuitionistic logic

This page was built for publication: A Formulae-as-Types Interpretation of Subtractive Logic

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