Co-induction in Relational Semantics

R. Milner and M. Tofte

Abstract: An application of the mathematical theory of maximum fixed points of monotonic set operators to relational semantics is presented. It is shown how an important proof method, called co-induction, can be used to prove the consistency of the static and the dynamic relational semantics of a small functional programming language with recursive functions.

LFCS report ECS-LFCS-88-65

This report was published in Theoretical Computer Science, 87(1), pp209-220, September 1990.

Previous | Index | Next