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

Favio Ezequiel Miranda-Perea
(Facultad de Ciencias UNAM)
Lourdes del Carmen González-Huesca
(Facultad de Ciencias UNAM)

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-Parigot by means of primitive (co)recursion principles. Our logic includes primitive constructors of least and greatest fixed points of predicate transformers, but contrary to the common approach, we do not restrict ourselves to positive operators to ensure monotonicity, instead we use the Mendler-style, motivated here by the concept of monotonization of an arbitrary operator on a complete lattice. We prove an adequacy theorem with respect to a realizability semantics based on saturated sets and saturated-valued functions and as a consequence we obtain the strong normalization property for the proof-term reduction, an important feature which is absent in previous related work.

In Simona Ronchi della Rocca and Elaine Pimentel: Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011), Belo Horizonte, Brazil, 27 August 2011, Electronic Proceedings in Theoretical Computer Science 81, pp. 30–46.
Published: 24th March 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.81.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org