Implementing parametricity in Rocq-ELPI
summary
Implements a sequent-calculus style binary parametricity as a logic program inside Rocq-ELPI, translating each inference rule to an ELPI clause that produces both the related term and its relation witness. Uses HOAS (Hokep) to avoid manual freshness and binder plumbing, handles lambdas by universally quantifying three fresh variables in the clause body, inserts trivial matches to make fixpoints constructor-headed, and generates shims to translate records; core implementation ships in the standard distribution but indexed/mutual-record support is still pending.
AI-written summary · about
chapters (10)
- 0:00Parametricity implementation
- 1:03Parametricity as code generation
- 3:54Challenges in implementation
- 5:20ELPI and HOAS for binders
- 6:24Sequent-style parametricity rules
- 7:46ELPI predicates for rules
- 8:50Scaling to Rocq features
- 10:37Records and inductive types
- 12:01Status and limitations
- 12:42Q&A
related talks
51mElpi: rule-based meta-languge for Rocq
19mType Inference Logics
47mLogic Programming à la Carte
34mLanguage Design Where Paradigms Meet
30mA Mechanised Semantics of Erlang’s References
28mSemi-explicit polymorphic parameters
25mA Relational Separation Logic for Effect Handlers
19mCertified Compilers à la Carte