Classical Logic with Mendler Induction

DOI10.1007/978-3-319-27683-0_4MaRDI QIDQ5283417zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A strong normalization result for classical logic
• Strong Normalization of the Dual Classical Sequent Calculus
• A note on strong normalization in classical natural deduction
• Classical logic with Mendler induction
• Strong normalization of classical natural deduction with disjunctions
• scientific article; zbMATH DE number 1722654
• Proofs of strong normalisation for second order classical natural deduction
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• scientific article; zbMATH DE number 2024631

Cites work

• scientific article; zbMATH DE number 1088045 (Why is no real title available?)
• scientific article; zbMATH DE number 2080223 (Why is no real title available?)
• scientific article; zbMATH DE number 1748069 (Why is no real title available?)
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• scientific article; zbMATH DE number 1400097 (Why is no real title available?)
• A Formulae-as-Types Interpretation of Subtractive Logic
• A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences
• A symmetric lambda calculus for classical program extraction
• Call-by-value is dual to call-by-name
• Dual Calculus with Inductive and Coinductive Types
• Fixed Point Logics
• Inductive types and type constraints in the second-order lambda calculus
• Investigations on the dual calculus
• Iteration and coiteration schemes for higher-order and nested datatypes
• Strong Normalization of the Dual Classical Sequent Calculus
• The duality of computation
• The power of parameterization in coinductive proof

Cited in

(2)

• Mendler-style iso-(co)inductive predicates: a strongly normalizing approach
• Classical logic with Mendler induction

Describes a project that uses

Uses Software

• Paco

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)