A co-induction principle for recursively defined domains

DOI10.1016/0304-3975(94)90014-0zbMath0795.68129OpenAlexW2010663699MaRDI QIDQ1318702

Andrew M. Pitts

Publication date: 5 April 1994

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

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90014-0

zbMATH Keywords

partial orderbisimulationsdenotational semanticsgreatest fixed pointco-induction principlehigher-order functional programming languagespowerdomain constructorsrecursively defined datatypesrecursively defined predomains

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Continuous lattices and posets, applications (06B35)

Related Items

Open maps, behavioural equivalences, and congruences, Codifying guarded definitions with recursive schemes, Safety of Nöcker's strictness analysis, Intuitionistic sets and ordinals, Strong categorical datatypes II: A term logic for categorical programming, Simulations in coalgebra, A fixedpoint approach to implementing (Co)inductive definitions, Coinductive big-step operational semantics, Structural induction and coinduction in a fibrational setting, Using a generalisation critic to find bisimulations for coinductive proofs, Universal coalgebra: A theory of systems, A type-theoretical alternative to ISWIM, CUCH, OWHY

Uses Software

• ML
• Haskell

Cites Work

• Co-induction in relational semantics
• Full abstraction in the lazy lambda calculus
• A domain equation for bisimulation
• The Category-Theoretic Solution of Recursive Domain Equations
• A Powerdomain Construction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item