Program equivalence is coinductive

DOI10.1145/2933575.2934506MaRDI QIDQ4635889zbMATH OpenOpenAlexWikidataFDO

Authors Dirk Pattinson, Lutz Schröder

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2933575.2934506

zbMATH Keywords

algebraic theoriescomodelsmodels of computationnon-wellfounded proofsprogram equivalence

Mathematics Subject Classification ID

Logic in computer science (03B70) Equational classes, universal algebra in model theory (03C05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Sound and complete equational reasoning over comodels
• A note on Coinduction and Weak Bisimilarity for While Programs
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• On coinductive equivalences for higher-order probabilistic functional programs
• A complete, co-inductive syntactic theory of sequential control and state

Cited in

(5)

• scientific article; zbMATH DE number 2090534 (Why is no real title available?)
• The costructure–cosemantics adjunction for comodels for computational effects
• Well-definedness and observational equivalence for inductive–coinductive programs
• Stream processors and comodels
• Sound and complete equational reasoning over comodels

Describes a project that uses

Uses Software

• Cyclist

This page was built for publication: Program equivalence is coinductive

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