A proof of Moessner's theorem by coinduction

DOI10.1007/S10990-012-9082-7MaRDI QIDQ1929334zbMATH OpenOpenAlexFDO

Authors Milad Niqui, Jan J. M. M. Rutten

Publication date 8 January 2013

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10990-012-9082-7

zbMATH Keywords

coalgebracoinductionMoessner's theoremstreamstream bisimulationstream calculusstream differential equation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
• A characterization of Moessner's sieve
• On Moessner's theorem
• Elements of stream calculus (an extensive exercise in coinduction)
• Moessnerian theorems. How to prove them by simple graph theoretical inspection

Cites work

• A coinductive calculus of streams
• Concrete stream calculus: an extended study
• scientific article; zbMATH DE number 41838 (Why is no real title available?)
• scientific article; zbMATH DE number 718142 (Why is no real title available?)
• scientific article; zbMATH DE number 3073057 (Why is no real title available?)
• scientific article; zbMATH DE number 3073058 (Why is no real title available?)
• Sampling, splitting and merging in coinductive stream calculus
• Universal coalgebra: A theory of systems

Cited in

(10)

• Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
• A characterization of Moessner's sieve
• Bisimulation and coinduction enhancements: a historical perspective
• Formalizing Moessner's theorem and generalizations in \textsc{Nuprl}
• The power of parameterization in coinductive proof
• Stream differential equations: specification formats and solution methods
• Newton series, coinductively: a comparative study of composition
• On Moessner's theorem
• Typed Lambda Calculi and Applications
• Moessnerian theorems. How to prove them by simple graph theoretical inspection

This page was built for publication: A proof of Moessner's theorem by coinduction

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