Build a Learning Habit
Download Class Central's free printable study calendar
Download for Free
In this Oxford Seminar from March 6, 2025, Owen Lynch presents a new Rust implementation of generalized algebraic theories that takes a more type-theoretic approach. Discover how this implementation integrates e-graphs into the type-checking process to enable extensive equality approximation and greater theory compositionality, achieving the long-desired "theory pushout" principle. Learn about the implementation's role as a prototype for type-checking algorithms intended for CatColab and enabling "open notebooks" for compositional modeling. The talk also explores how lessons from this two-level type theory implementation could apply to various domains requiring abstraction without complicating underlying semantics, including finite state machines, probabilistic programming, SAT solving, systems programming, constraint programming, databases, and serialization formats. This seminar builds on Topos Institute's long-standing work with generalized algebraic theories, dating back to the beginnings of Catlab.jl.
