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
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Monday, July 14, 2014 - 2:18:24 AM
Last modification on : Saturday, June 25, 2022 - 8:54:34 PM
Long-term archiving on: : Friday, November 21, 2014 - 2:23:37 PM


Files produced by the author(s)



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⟩



Record views


Files downloads