Classical Logic with Mendler Induction

DOI10.1007/978-3-319-27683-0_4zbMATH Open1476.03008OpenAlexW2343288535MaRDI QIDQ5283417FDOQ5283417

Marcelo P. Fiore, Marco Devesas Campos

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)

Cites Work

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

Uses Software

• Paco

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem 👍 👎
• Proofs of strong normalisation for second order classical natural deduction 👍 👎
• Strong normalization of classical natural deduction with disjunctions 👍 👎
• Strong Normalization of the Dual Classical Sequent Calculus 👍 👎
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction 👍 👎
• A strong normalization result for classical logic 👍 👎
• Classical logic with Mendler induction 👍 👎

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5283417)