Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme

DOI10.1007/978-3-642-02444-3_17zbMath1246.68199OpenAlexW1549054207MaRDI QIDQ3638258

Milad Niqui

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02444-3_17

zbMATH Keywords

coalgebrabisimulationcoinductionCoqcoiteration

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Universal coalgebra: A theory of systems
• The music of streams
• Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
• Inductive and Coinductive Components of Corecursive Functions in Coq
• Modular Development of Hybrid Systems for Verification in Coq
• Using Structural Recursion for Corecursion
• An induction principle for nested datatypes in intensional type theory
• A coinductive calculus of streams
• Generalised Coinduction
• Semi-continuous Sized Types and Termination

This page was built for publication: Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme