Mendler-style Iso-(Co)inductive predicates: a strongly normalizing approach

Favio Ezequiel Miranda-Perea, Lourdes del Carmen González-Huesca

We present an extension of the second-order logic AF2 with iso-style inductive and coinductive definitions specifically designed to extract programs from proofs a la Krivine-Parigo…