Classical logic with Mendler induction

Reference. Classical logic with Mendler induction

Marco Devesas Campos, Marcelo P. Fiore · Journal of Logic and Computation · 2020 · DOI

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 and show that it is strongly normalizing. We prove this using a reducibility argument.

Cite

Cite as @devesascampos-2020-classical (helia, typst) · \cite{devesascampos-2020-classical} (LaTeX)

BibTeX

bibtex · 1 line

@article{devesascampos-2020-classical, title={Classical logic with Mendler induction}, volume={30}, ISSN={1465-363X}, url={http://dx.doi.org/10.1093/logcom/exaa004}, DOI={10.1093/logcom/exaa004}, number={1}, journal={Journal of Logic and Computation}, publisher={Oxford University Press (OUP)}, author={Devesas Campos, Marco and Fiore, Marcelo}, year={2020}, month=Jan, pages={77–106} }

hayagriva YAML (typst)

yaml · 18 lines

devesascampos-2020-classical:
  type: article
  title: Classical logic with Mendler induction
  author:
  - Devesas Campos, Marco
  - Fiore, Marcelo
  date: 2020-01
  page-range: 77-106
  url: http://dx.doi.org/10.1093/logcom/exaa004
  serial-number:
    doi: 10.1093/logcom/exaa004
    issn: 1465-363X
  parent:
    type: periodical
    title: Journal of Logic and Computation
    publisher: Oxford University Press (OUP)
    issue: 1
    volume: 30

Download: devesascampos-2020-classical.bib · devesascampos-2020-classical.yml

Cites 22 works (0 here)

External (22)

Mendler Induction and Classical Logic (2015)
The power of parameterization in coinductive proof (2013)
A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences (2011)
Dual calculus with inductive and coinductive types (2009)
Investigations on the dual calculus (2006)
Iteration and coiteration schemes for higher-order and nested datatypes (2005)
Strong normalization of the dual classical sequent calculus (2005)
A formulae-as-types interpretation of subtractive logic (2004)
Call-by-value is dual to call-by-name (2003)
Introduction to Lattices and Order (2002)
Fixed point logics (2002)
The duality of computation (2000)
Strong normalization of second order symmetric $\lambda $ calculus (2000)
Mendler-style inductive types, categorically (1999)
Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types (1998)
‘Classical’ programming-with-proofs in $\lambda ^Sym_PA$. An analysis of non-confluence (1997)
A tutorial on (co) algebras and (co) induction (1997)
A symmetric lambda calculus for classical program extraction (1996)
ML with callcc is unsound (1991)
Inductive types and type constraints in the second-order lambda calculus (1991)
Abstract types have existential type (1988)
Investigations into logical deduction (1964)