Program equivalence is coinductive

DOI10.1145/2933575.2934506zbMATH Open1401.68084OpenAlexW2530648415WikidataQ130970088 ScholiaQ130970088MaRDI QIDQ4635889FDOQ4635889

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

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

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)

Cited In (4)

• Well-definedness and observational equivalence for inductive–coinductive programs
• Title not available (Why is that?)
• Stream processors and comodels
• The costructure–cosemantics adjunction for comodels for computational effects

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)