Admissible Types-to-PERs Relativization in Higher-Order Logic

on YouTube ↗28m

" summary

Proves that for a large practical fragment of HOL (including datatypes and codatatypes) a types-to-PERs relativization is admissible: if a type-based theorem is provable then its PER-relativized counterpart is provable. Defines a relational interpretation, requires a whiteness (largeness) condition on type definitions, and shows common library types (e.g. polynomials) satisfy it. Implements a prototype Isabelle tool that performs relativization on demand (currently emits axiomatized relativized theorems but can generate proofs if proof objects are enabled).

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 0:47Proof Assistants, a.k.a. Interactive Theorem Provers
3. 1:43Verification Success Stories
4. 3:23Two Little Pigs
5. 7:36HOL in One Slide
6. 10:07HOL in Practice
7. 10:58Back to
8. 13:17Towards a General Definition of Types-To-Sets
9. 18:25Summary of the Desiderata for Relativization
10. 19:58Defining RIN: Type→ Term and RLT: Term → Term
11. 24:29Relativization Infrastructure
12. 25:11Related Work