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 theoriesmodels of computationprogram equivalencenon-wellfounded proofscomodels

Mathematics Subject Classification ID

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

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)

• Well-definedness and observational equivalence for inductive–coinductive programs
• scientific article; zbMATH DE number 2090534 (Why is no real title available?)
• Stream processors and comodels
• The costructure–cosemantics adjunction for comodels for computational effects
• 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)