Coalgebra for the working programming languages researcher
summary
Coalgebraic methods center on a functor that generates syntax, denotational and operational semantics, and equivalence proofs; from that one structure researchers derive concrete algorithms such as the NetKAT POPL’15 algorithm for network language equivalence and NFA checks based on bisimulation up to congruence that outperform bespoke algorithms. Implementations exist as pieces: the circ/K-framework work, Coq libraries and OCaml/co‑pattern extensions, and follow‑up papers (POPL’17 learning extensions, PLDI’19 MacNetKAT fragment) show the approach yields practical, provably correct tools.
AI-written summary · about
chapters (4)
related talks
19mGraphCoQL: A mechanized formalization of GraphQL in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
21mIntrinsically Correct Algorithms and Recursive Coalgebras
01h 34mFormal Logic Undressed
30mCalculating Compilers for Concurrency
19mExtensible Metatheory Mechanization via Family Polymorphism
24mCode Extraction from Coq to ML-like languages