Examples of Restriction Spaces

In this session, a number of examples are provided to illustrate how the Restriction_Spaces library works. The simple cases are, of course, covered: trivial restriction, booleans, integers, option type, and so on. But we also explore more elaborate constructions, such as formal power series and a trace model of the CSP process algebra. Additionally, we provide a lightweight integration with HOLCF, equipping restriction spaces with the inherited partial order structure when needed.