reading list
- ☐ Separation and information hiding
- ☐ Semantics of Separation-Logic Typing and Higher-Order Frame Rules
- ☐ Relational Parametricity and Separation Logic
- ☐ The category-theoretic solution of recursive metric-space equations
- ☐ Modular Denotational Semantics for Effects with Guarded Interaction Trees
- ☐ Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
- ☐ Program Logics à la Carte
- ☐ The Call-by-Need Lambda Calculus
- ☐ An Adequate Operational Semantics of Sharing in Lazy Evaluation
- ☐ Computational Comonads and Intensional Semantics