Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with(…)

on YouTube ↗19m

" summary

Provides a semantic criterion that turns inductive rule systems with binders into strengthened induction theorems by modelling relations as Knaster–Tarski fixed points and requiring nominal-set structure plus equivariance and refreshability. Implements this in Isabelle/HOL with a heuristic that often proves the criterion automatically, produces fresh-variable assumptions rather than forcing side-conditions, and handles infinitary and non-equivariant syntax. Validated on beta reduction, transitivity of subtyping, pi-calculus reduction, and an infinite lambda-calculus formalisation.

AI-written summary · about

" chapters (15)

1. 0:00Introduction
2. 0:21Binder relations problem
3. 1:44Theorem prover status quo
4. 3:51Contributions and approach
5. 4:32Relations as fixed points
6. 6:18Binders in fixed points
7. 7:02Nominal set criteria
8. 8:48Equivariance and refreshability
9. 9:30Beta fresh induction theorem
10. 10:11User experience in Isabelle
11. 11:14New approach advantages
12. 12:17Case studies validation
13. 12:57Foundations and related work
14. 13:17Summary
15. 13:41Q&A