Trocq parametricity translations for inductives (RocqPL 2026 - Rocq for Programming Languages 2026) - POPL 2026

Sun 11 - Sat 17 January 2026 Rennes, France

Track

RocqPL 2026 Rocq for Programming Languages

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Sat 17 Jan 2026 15:00 - 15:15 at Salle 14 - Rocq Enhancements and Extensions

Abstract

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.

File attachments

Extended Abstract (rocqpl26-final6.pdf)	469KiB

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

	14:00 - 15:30	Rocq Enhancements and ExtensionsRocqPL at Salle 14

	14:00 15m Talk		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 15m Talk		Implementing parametricity in Rocq-ELPI RocqPL Cyril Cohen Inria, CNRS, ENS Lyon, UCBL, LIP, Vojtěch Štěpančík Inria
	14:30 15m Talk		Enhancing universe polymorphism for Rocq: Algebraic universes, consistency checking and variance inference RocqPL Matthieu Sozeau Inria, Marc Bezem University of Bergen File Attached
	14:45 15m Talk		Nested Inductive Types for Rocq and Lean RocqPL Thomas Lamiaux Nantes Université, Inria, Yannick Forster INRIA, Matthieu Sozeau Inria, Nicolas Tabareau Inria
	15:00 15m Talk		Trocq parametricity translations for inductives RocqPL Tomas Vallejos Parada Inria File Attached
	15:15 15m Talk		Verifying Synchronous Dataflow Programs with SMTCoq RocqPL Basile Pesin Ecole Nationale de l'Aviation Civile (ENAC) File Attached

Hide past events

Tomas Vallejos Parada

Inria