Library cawu.ccs
Library cawu.streams
- Example: Rutten's stream calculus
- "constant" streams
- pointwise sum and its properties
- shuffle product
- convolution product
Library cawu.divergence
Library cawu.rel
- Utilities for working with binary relations
- Pairs and sets of pairs
- Friendly coinduction tactic, for relations
- Generic definitions and results about relations
- Contexts
Library cawu.coinduction
- Coinduction All the Way Up
- Knaster-Tarski and compatibility
- Compatibility up-to: second order reasoning
- Parametric coinduction: the accumulation rule
- Symmetry arguments
- Proof system
- Coincidence of the greatest respectful and the greatest compatible
- Characterisation of Hur et al.' function G using the companion
Library cawu.lattice
This page has been generated by coqdoc