Mendler-style iso-(co)inductive predicates: a strongly normalizing approach

zbMATH Open1458.68039arXiv1203.6158MaRDI QIDQ5858675FDOQ5858675

Authors: Favio E. Miranda Perea, Lourdes del Carmen González Huesca 

Publication date: 14 April 2021

Full work available at URL: https://arxiv.org/abs/1203.6158

Recommendations

• Classical Logic with Mendler Induction
• Classical logic with Mendler induction
• A direct proof of strong normalization for full constructive second-order logic
• scientific article; zbMATH DE number 1696607
• Extended Curry-Howard terms for second-order logic

zbMATH Keywords

strong normalizationsecond-order logicsaturated setmonotonizationprogramming with proofs(co)inductive definitionsMendler-styleprimitive (co)recursion

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Higher-order logic (03B16) Logic in computer science (03B70)

Cited In (2)

• A realizability interpretation of Church's simple theory of types
• Classical logic with Mendler induction

This page was built for publication: Mendler-style iso-(co)inductive predicates: a strongly normalizing approach

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