Incremental pattern-based coinduction for process algebra and its Isabelle formalization

DOI10.1007/978-3-642-12032-9_9MaRDI QIDQ3557847zbMATH OpenOpenAlexFDO

Authors Andrei Popescu, Elsa Gunter

Publication date 27 April 2010

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-12032-9_9

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Fundamental Approaches to Software Engineering
• Coalgebraic bisimulation-up-to
• scientific article; zbMATH DE number 1361141
• A general account of coinduction up-to
• Using a generalisation critic to find bisimulations for coinductive proofs

Cited in

(9)

• A formalized general theory of syntax with bindings
• A formalized general theory of syntax with bindings: extended version
• Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
• Processes as formal power series: a coinductive approach to denotational semantics
• scientific article; zbMATH DE number 1361141 (Why is no real title available?)
• scientific article; zbMATH DE number 1942459 (Why is no real title available?)
• Using a generalisation critic to find bisimulations for coinductive proofs
• Fundamental Approaches to Software Engineering
• A contextual formalization of structural coinduction

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• CIRC

This page was built for publication: Incremental pattern-based coinduction for process algebra and its Isabelle formalization

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