Sciweavers

Share
LFCS
2016
Springer

Classical Logic with Mendler Induction - A Dual Calculus and Its Strong Normalization

4 years 3 months ago
Classical Logic with Mendler Induction - A Dual Calculus and Its Strong Normalization
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.
Marco Devesas Campos, Marcelo P. Fiore
Added 07 Apr 2016
Updated 07 Apr 2016
Type Journal
Year 2016
Where LFCS
Authors Marco Devesas Campos, Marcelo P. Fiore
Comments (0)
books