The 2026 Netherlands Winter School on Logic and Verification will take place Tuesday 20-Friday 23 January, 2026 at University of Twente. The school provides classes for PhD/graduate students in theoretical computer science, with a focus on software verification, logic, and type theory. Strong master students, as well as researchers and practitioners, are equally welcome. Participants are expected to have a background in theoretical computer science, mathematics or a related discipline at a master’s level, and have basic familiarity with (functional) programming, semantics, and logic.
cyclic-structures.gitlab.io/school2026/
Please consider registering! If you're a PhD student registered with the IPA school it will (very likely) be possible to get the costs reimbursed, but anyone with their own funding is welcome too.
#Logic #Verification #TypeTheory #CategoryTheory #Coinduction #SessionTypes #Concurrency #Rocq #Agda #Iris
#Coinduction
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."
Ugh, we are finishing up a paper for submission and one of my coauthors wanted to better understand the math that I produced and get more useful references for people unfamiliar with #coinduction. Unfortunately it seems that by grabbing two approaches that try to treat it as something natural and combining them I did something that no one else did before, so now every reference will be confusing, because it uses an at least slightly different approach...
How are we going to find reviewers for that. :blobfoxmeltsob:
How are we going to find reviewers for that. :blobfoxmeltsob:
Client Info
Server: https://mastodon.social
Version: 2025.07
Repository: https://github.com/cyevgeniy/lmst