Explore a 21-minute conference talk from ACM SIGPLAN's CoqPL'24 event, focusing on a Coq library for reasoning about variable binding in programming languages. Delve into Piotr Polesiuk and Filip Sieczkowski's presentation on functorial syntax, a variant of Fiore, Plotkin, and Turi's approach. Learn about the development and practical applications of this library across various formalization projects, gaining insights into advanced techniques for representing and reasoning about binding structures in theorem proving systems.
Functorial Syntax for All - Representing and Reasoning About Binding Structures
ACM SIGPLAN via YouTube
Overview
Syllabus
[CoqPL'24] Functorial Syntax for All
Taught by
ACM SIGPLAN