POPL 2026 (series) / RocqPL 2026 (series) / Rocq for Programming Languages 2026 /
Trocq parametricity translations for inductives
Sat 17 Jan 2026 15:00 - 15:15 at Salle 14 - Rocq Enhancements and Extensions Chair(s): Frédéric Besson
This submission describes an extension of the Trocq plugin for proof transfer. It automates the generation of the lattice of parametricity translations from the Trocq hierarchy for a significant class of inductive types, thus removing this burden from the user.
| Extended Abstract (rocqpl26-final6.pdf) | 469KiB |
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | |||
14:00 15mTalk | A systematic approach to "Well-founded recursion done right" RocqPL Herman Geuvers Radboud University Nijmegen, Netherlands, Gijs Pennings Eindhoven University of Technology File Attached | ||
14:15 15mTalk | Implementing parametricity in Rocq-ELPI RocqPL File Attached | ||
14:30 15mTalk | Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking and variance inference RocqPL File Attached | ||
14:45 15mTalk | Nested Inductive Types for Rocq and Lean RocqPL Thomas Lamiaux Nantes Université, Inria, Yannick Forster INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria | ||
15:00 15mTalk | Trocq parametricity translations for inductives RocqPL Tomas Vallejos Parada Inria File Attached | ||
15:15 15mTalk | Verifying Synchronous Dataflow Programs with SMTCoq RocqPL Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC) File Attached | ||