This site collects information about positions, publications and relevant news for the project “Cyclic Structures in Programs and Proofs” project, funded by NWO. The project aims to advance the theory of cyclic structures in proofs and programs, including in coalgebraic modal logic, type theory, behavioural types, and the proof assistants Agda and Rocq (formely Coq), and create a development environment for Rust based on these techniques.
3/3 Codata Applications:
This approach is particularly useful for:
- Representing infinite structures (e.g., streams)
- Encoding constraints (via indexed codata)
- Implementing lazy evaluation in strict languages
- Representing thunks or constructs like Lazy, Delay, or Later
2/3 Continuing on Codata:
- Like operations on a Java interface: define how to get values out, caller chooses which operation to call
- You construct an object with computations (methods) to produce values on demand
Key distinction:
- You consume (destruct) data by pattern matching on a value
- You construct codata by providing computations to implement the destructors
1/3 Demystifying Codata (or coinduction):
In strict functional programming, we typically think about:
- Values (data): constructed upfront, directly visible, accessible
- Computations (functions): consume/destruct data, opaque
Codata flips this around:
- We define how to observe/destruct it
- Construction happens on-demand when observed (observed = selecting one of the methods in the object to call)
Paper by Ivan Todorov and Casper Bach Poulsen at TyDe '24: Modal μ-Calculus for Free in Agda
"Using dependently-typed programming in Agda, we develop an embedding of the modal μ-calculus for defining and verifying functional properties of possibly-non-terminating effectful programs which we represent in Agda using the coinductive free monad."
Jesper Agdakx 🔸
Yuri Not Igor
Programming Languages Delft
timorl