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

zbMATH Open1458.68039MaRDI 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

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)

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

Cited in

(2)

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

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)