🍞 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	Kind
Staton 2025	Every Hoare rule is a theorem, not an axiom — derived from categorical axioms (correctness, incorrectness, relational)	→	🍞
Fritz 2020	Stochastic functions form a category with copy and discard	→	🍞
Fritz, Perrone, Rezagholi 2021	"Which outputs are possible?" is a monad morphism	→	🍞
Gaboardi, Katsumata, Orchard, Sato 2021	Hoare logic with grades: track side effects through composition	→	🍞
Kura, Gaboardi, Sekiyama, Unno 2026	Effects that depend on values: indexed graded monads for dependent effect systems	→	🍞
Ghani, Hedges, Winschel, Zahn 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 give rise to Markov categories (compositional imprecise probability)	→	🍞
Sato, Katsumata 2023	Distance between programs = enrichment on the category	→	🍞
Spivak 2013	Typed ports and wiring diagrams: the syntax layer for composing boxes	→	🍞
Aguirre, Katsumata, Kura 2022	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	Separation logic for Bayesian programs: the frame rule IS probabilistic independence	→	🍞
Chen, Vigneaux 2023	Shannon entropy and magnitude unified: recovers magnitude under uniform	→	🍞

≈ proven equivalence — a theorem makes the two sides the same structure · → construction — one side builds on / gives rise to the other · ~ framing — an intuition or lens, not a proven equivalence

🪞 The negative space: Neat, Not Useful — where these same bridges hold and still drop their cargo, and the three ways a translation fails.

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