Functorial Syntax for All - Representing and Reasoning About Binding Structures

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.