Classical Logic with Mendler Induction

DOI10.1007/978-3-319-27683-0_4zbMath1476.03008OpenAlexW2343288535MaRDI QIDQ5283417

Marco Devesas Campos, Marcelo P. Fiore

Publication date: 21 July 2017

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-27683-0_4

zbMATH Keywords

realizabilityCurry-Howard isomorphismclassical logicdual calculusMendler induction

Mathematics Subject Classification ID

Type theory (03B38)

Uses Software

• Paco

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Iteration and coiteration schemes for higher-order and nested datatypes
• A symmetric lambda calculus for classical program extraction
• Investigations on the dual calculus
• Inductive types and type constraints in the second-order lambda calculus
• The power of parameterization in coinductive proof
• The duality of computation
• Dual Calculus with Inductive and Coinductive Types
• Fixed Point Logics
• A Formulae-as-Types Interpretation of Subtractive Logic
• A hierarchy of mendler style recursion combinators
• Call-by-value is dual to call-by-name
• Strong Normalization of the Dual Classical Sequent Calculus

This page was built for publication: Classical Logic with Mendler Induction