Trocq parametricity translations for inductives
summary
Claims an extension to the Trocq plugin that automatically generates the lattice of parametricity translations for inductive types with parameters and recursion but no indices yet, building bottom-up to produce the maps and projection proofs at every lattice level (M0 up to equivalences) and thus avoids using univalence when possible. Implementation composes the binary parametricity and derive plugins, is available on a personal fork of the Trocq repo, and demonstrates working examples for nat and lists.
AI-written summary · about
chapters (6)
- 0:00Trocq and parametricity intro
- 1:46Type translation motivation
- 3:59Automatic relation derivation
- 7:32Lattice derivation strategy
- 9:23Natural numbers example
- 12:00Q&A
related talks
19mExtensible Metatheory Mechanization via Family Polymorphism
22mA Calculus of Inductive Linear Constructions
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
21mFunctorial Syntax for All
25mDeriving Instances with Dependent Types
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
28mSemi-explicit polymorphic parameters
19mInterpreting OCaml GADTs into Coq