Computer Science – Logic in Computer Science
Scientific paper
2012-03-28
EPTCS 81, 2012, pp. 30-46
Computer Science
Logic in Computer Science
In Proceedings LSFA 2011, arXiv:1203.5423
Scientific paper
10.4204/EPTCS.81.3
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.
Carmen González-Huesca Lourdes del
Miranda-Perea Favio Ezequiel
No associations
LandOfFree
Mendler-style Iso-(Co)inductive predicates: a strongly normalizing approach does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Mendler-style Iso-(Co)inductive predicates: a strongly normalizing approach, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Mendler-style Iso-(Co)inductive predicates: a strongly normalizing approach will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-271835