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.
This report was published in Theoretical Computer Science, 87(1), pp209-220, September 1990.
Previous | Index | Next An error occured whilst processing this directive