🍞 Natural Breadcrumbs

Applied category theory and programming language theory are converging on the same structures from different directions. These pages map the translations, with runnable code.

PL theory

assert P(x)
y = f(x)
assert R(y)
z = g(y)
assert Q(z)

Category theory

{ P } f { R }    { R } g { Q }
─────────────────────
    { P } g∘f { Q }

Same structure. Different notation. Each paper below gets a page that shows both.

Papers

Each paper has a 🍞 page that translates its key ideas into diagrams and runnable code.

Paper	One sentence
Staton 2025	Every Hoare rule is a theorem, not an axiom, in stochastic systems	🍞
Fritz 2020	Stochastic functions form a category with copy and discard	🍞
Fritz, Perrone, Rezagholi 2021	"Which outputs are possible?" is a monad morphism	🍞
Gaboardi 2021	Hoare logic with grades: track side effects through composition	🍞
Kura 2026	Stage N's guarantee becomes stage N+1's assumption	🍞
Hedges, Ghani 2018	Nash equilibrium composes the same way contracts compose	🍞
Capucci 2021	"What is a goal but a predicate on a system?"	🍞
Baez, Fritz, Leinster 2011	Shannon entropy is the only information loss that respects composition	🍞
Liell-Cock, Staton 2025	Graded monads and Markov categories are the same structure	🍞
Sato, Katsumata 2023	Distance between programs = enrichment on the category	🍞
Spivak 2013	Typed ports and wiring diagrams: the syntax layer for composing boxes	🍞
Jacobs 2014	Weakest preconditions from fibrations over Kleisli categories	🍞
Kidney, Wu 2021	One monad parameterized by a semiring: probability, counting, search	🍞
Leinster 2021	Diversity IS categorical cardinality: magnitude generalizes species count	🍞
Smithe 2021	Bayesian inversions compose as lenses: forward inference, backward learning	🍞
Parzygnat 2020	Bayesian inversion as dagger structure: three levels of reversibility	🍞
Di Lavore, Roman, Sobocinski 2025	Markov categories where morphisms can fail: observations, conditioning	🍞
Panangaden 2009	Bisimulation metrics: behavioral distance between stochastic processes	🍞
Cho, Jacobs 2015	Predicates as effects, not subobjects: states/effects duality	🍞
Ho, Wu, Raad 2026	Hoare logic for Bayesian programs: frame rule IS probabilistic independence	🍞
Chen, Vigneaux 2023	Shannon entropy and magnitude unified: recovers magnitude under uniform	🍞

Three ways in

A Lean 4 proof machine-checks the connections (read the proof file by file)
A vocabulary table maps terms across communities
This site: the same ideas, in code you can run

Also: symbol grid · how to use this site

📺 Video lectures: MIT 18.S097: Applied Category Theory (Fong & Spivak) · Stanford CS364A: Algorithmic Game Theory (Roughgarden)

Neighbors

🐱 Category Theory — the mathematical language most papers use
🎰 Probability — probability monads and Markov kernels throughout
📡 Information Theory — entropy as a functor is central
✏️ Lean Proofs — several results formalized