Skip to Main content Skip to Navigation
Conference papers

Formulae-as-Types for an Involutive Negation

Abstract : Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements. We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the ℓ delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between A and ¬¬A, and thus between ¬∀ and ∃¬.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00996742
Contributor : Guillaume Munch-Maccagnoni <>
Submitted on : Monday, July 14, 2014 - 2:18:24 AM
Last modification on : Saturday, February 15, 2020 - 2:04:11 AM
Long-term archiving on: : Friday, November 21, 2014 - 2:23:37 PM

File

involutive.pdf
Files produced by the author(s)

Identifiers

Citation

Guillaume Munch-Maccagnoni. Formulae-as-Types for an Involutive Negation. Joint meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603156⟩. ⟨hal-00996742v2⟩

Share

Metrics

Record views

435

Files downloads

568