Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

Watch this 19-minute conference talk from POPL 2025 that presents a significant contribution to the meta-theory of systems featuring syntax with bindings. Learn about a general criterion for inductively defined rule-based systems that enables proofs leveraging Barendregt's variable convention of keeping bound and free variables disjoint. The presentation, delivered by researchers from Heriot-Watt University, University of Sheffield, and University of Copenhagen, improves on existing approaches by achieving high generality using Knaster-Tarski fixed point definitions, capturing systems of interest without modifications, and accommodating infinitary syntax and non-equivariant predicates. The talk is accompanied by reusable artifacts available through Zenodo, making it valuable for researchers working on formal reasoning, nominal sets, and syntax with bindings.