Co-induction in relational semantics (Q1177158)

The purpose of this paper is to present the use of non-well-founded sets in the study of programming languages semantics. The authors show how co- induction may be used for proving properties of non-well-founded sets (objects), in a similar way how induction is used for classical well- founded sets. Co-induction is presented as a variant of the fixpoint induction principle of Park. In the paper, co-induction is an important proof technique associated with the maximum fixed point of a monotonic operator. This technique is used to prove the consistency of the static and the dynamic relational semantics for a functional programming language. This language is essentially the lambda calculus with an explicit construction for recursive functions.