## 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