Co-Induction in Relational Semantics

Robin Milner, Mads Tofte

Research output: Contribution to journalArticlepeer-review


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 which we call co-induction, a variant of Park's (1969) principle of fixpoint 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.
Original languageEnglish
Pages (from-to)209-220
Number of pages12
JournalTheoretical Computer Science
Issue number1
Publication statusPublished - Sep 1991

Fingerprint Dive into the research topics of 'Co-Induction in Relational Semantics'. Together they form a unique fingerprint.

Cite this