Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

19

LFCS
2016
Springer

favoriteEmaildiscussreport

52views Artificial Intelligence» more LFCS 2016»

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

8 years 1 months ago

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

Download www.cl.cam.ac.uk

We investigate (co-)induction in Classical Logic under the propositions-as-types paradigm, considering propositional, second-order, and (co-)inductive types. Speciﬁcally, 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

Real-time Traffic

Artificial Intelligence | LFCS 2016 |

claim paper

Related Content

» Strong Normalization of the Dual Classical Sequent Calculus

» Strong normalization of a symmetric lambda calculus for secondorder classical logic

» On Strong Normalization of the Calculus of Constructions with TypeBased Termination

» Classical BI Its Semantics and Proof Theory

» Generalized Iteration and Coiteration for HigherOrder Nested Datatypes

» Naming Proofs in Classical Propositional Logic

» A Logical Foundation for Environment Classifiers

Post Info
More Details (n/a)

Added	07 Apr 2016
Updated	07 Apr 2016
Type	Journal
Year	2016
Where	LFCS
Authors	Marco Devesas Campos, Marcelo P. Fiore

Comments (0)