Co-induction in relational semantics

DOI10.1016/0304-3975(91)90033-XMaRDI QIDQ1177158zbMATH OpenOpenAlexFDO

Authors M. Tofte, Robin Milner

Publication date 26 June 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90033-x, https://www.pure.ed.ac.uk/ws/files/15220807/Co_induction_in_relational_semantics.pdf

zbMATH Keywords

fixpoint inductionfunctional programming languagerecursive functions

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Review text

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.

Recommendations

• On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces
• Nonwellfounded sets and programming language semantics
• Practical coinduction
• Coinductive Logic Programming and Its Applications

Cites work

• A calculus of communicating systems
• A theory of type polymorphism in programming
• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 3349291 (Why is no real title available?)
• Type inference for polymorphic references

Cited in

(28)

• Coinductive big-step operational semantics
• A co-induction principle for recursively defined domains
• A simplified account of polymorphic references
• Universal coalgebra: A theory of systems
• A proof method for the correctness of modularized 0CFA
• Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
• A hidden Herbrand theorem: Combining the object and logic paradigms
• Non-well-founded deduction for induction and coinduction
• The fixed-point theory of strictly causal functions
• Bisimulation and coinduction enhancements: a historical perspective
• Final coalgebras and the Hennessy-Milner property
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Generalizing inference systems by coaxioms
• scientific article; zbMATH DE number 7037626 (Why is no real title available?)
• A co-inductive language and truth degrees
• Using a generalisation critic to find bisimulations for coinductive proofs
• Practical coinduction
• Proof methods for corecursive programs
• Simple type inference for term graph rewriting systems
• A structural co-induction theorem
• Control-flow analysis of function calls and returns by abstract interpretation
• A concrete final coalgebra theorem for ZF set theory
• Infinite objects in type theory
• Nonwellfounded sets and programming language semantics
• Checking equivalence of corecursive streams: an inductive procedure
• Timers for distributed systems
• Strong induction is an up-to technique
• Type inference for polymorphic references

Describes a project that uses

Uses Software

• ML

This page was built for publication: Co-induction in relational semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1177158)