A Formulae-as-Types Interpretation of Subtractive Logic

DOI10.1093/logcom/14.4.529zbMath1050.03007OpenAlexW3048760744MaRDI QIDQ4823807

Tristan 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

subtractive logicCurry-Howard isomorphismcontrol operatorscoroutines

Mathematics Subject Classification ID

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

Related Items (14)

Classical Logic with Mendler Induction ⋮ Hennessy-Milner properties via topological compactness ⋮ Natural deduction for bi-intuitionistic logic ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Dualized Simple Type Theory ⋮ Pragmatic and dialogic interpretations of bi-intuitionism. Part I ⋮ The semi Heyting-Brouwer logic ⋮ A type-theoretic foundation of delimited continuations ⋮ A Connection-Based Characterization of Bi-intuitionistic Validity ⋮ Deep Inference in Bi-intuitionistic Logic ⋮ Intuitionistic Letcc via Labelled Deduction ⋮ Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory ⋮ On the Computational Representation of Classical Logical Connectives ⋮ A connection-based characterization of bi-intuitionistic validity

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