Bisimulations generated from corecursive equations

DOI10.1016/J.ENTCS.2010.08.015MaRDI QIDQ3178257zbMATH OpenOpenAlexFDO

Authors Venanzio Capretta

Publication date 8 July 2016

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

Full work available at URL https://doi.org/10.1016/j.entcs.2010.08.015

zbMATH Keywords

coalgebrabisimulationcorecursionstreams

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Recommendations

• Corecursive algebras: a study of general structured corecursion
• Equations, contractions, and unique solutions
• Equations, contractions, and unique solutions
• Unguardedness mostly means many solutions
• Relating two approaches to coinductive solution of recursive equations

Cites work

• scientific article; zbMATH DE number 4047683 (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?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A calculus of communicating systems
• A coinductive calculus of streams
• A final coalgebra theorem
• Algebra and coalgebra in computer science. Third international conference, CALCO 2009, Udine, Italy, September 7--10, 2009. Proceedings
• Behavioural Differential Equations and Coinduction for Binary Trees
• Circular coinduction: a proof theoretical foundation
• Dependently typed programming in Agda
• Functional pearl: streams and unique fixed points
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Observational coalgebras and complete sets of co-operations
• Productivity of Stream Definitions
• Proof methods for corecursive programs
• Relating coalgebraic notions of bisimulation. With applications to name-passing process calculi (extended abstract)
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• Types for proofs and programs. International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994. Selected papers
• Well-Definedness of Streams by Termination

Cited in

(7)

• Bisimulations and bisimulation quotients of generalized Veltman models
• Unguardedness mostly means many solutions
• From rewrite rules to bisimulation congruences
• Coalgebras in functional programming and type theory
• Bisimulation proof methods in a path-based specification language for polynomial coalgebras
• Bisimulation Congruences in the Calculus of Looping Sequences
• Calculating Invariants as Coreflexive Bisimulations

Describes a project that uses

Uses Software

• Agda
• CIRC
• Coq

This page was built for publication: Bisimulations generated from corecursive equations

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