Classical logic with mendler induction a dual calculus and its strong normalization
Type
Conference Object
Change log
Authors
Campos, MD
Fiore, Marcelo https://orcid.org/0000-0001-8558-3492
Abstract
We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering propositional, second-order, and (co-)inductive types. Specifically, we introduce an extension of the Dual Calculus with a Mendler-style (co-)iterator that remains strongly normalizing under head reduction. We prove this using a non-constructive realizability argument.
Description
Keywords
Mendler Induction, Classical Logic, Curry-Howard isomorphism, Dual Calculus, Realizability
Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
Journal ISSN
0302-9743
1611-3349
1611-3349
Volume Title
9537
Publisher
Springer International Publishing