POPL 2026 (series) / RocqPL 2026 (series) / Rocq for Programming Languages 2026 /
Scalable Type Inference for Intrinsically-Typed Binders
Sat 17 Jan 2026 12:00 - 12:15 at Salle 14 - Rocq Developer Session and Mechanized Metatheory in Rocq Chair(s): François Pottier
Programming language design is one of the most important application domains for the Rocq prover yet scalable type inference for newly defined languages does not come easy. We propose a new approach called guided type inference that leverages bi-directionality hints and Ltac2 to infer types even for intrinsically-typed binders.
| Extended Abstract (rocqpl26-paper5.pdf) | 173KiB |
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | Rocq Developer Session and Mechanized Metatheory in RocqRocqPL at Salle 14 Chair(s): François Pottier Inria | ||
11:00 45mPanel | Session with the Rocq Development Team RocqPL | ||
11:45 15mTalk | Rocq CARVe-ing: A Library for Substructural Meta-Theory RocqPL Daniel Zackon McGill University, Ryan Kavanagh Université du Québec à Montréal, Alberto Momigliano Università degli Studi di Milano, Brigitte Pientka McGill University File Attached | ||
12:00 15mTalk | Scalable Type Inference for Intrinsically-Typed Binders RocqPL Max Kurze Barkhausen Institut, Clément Pit-Claudel EPFL, Sebastian Ertel Barkhausen Institute, Dresden File Attached | ||
12:15 15mTalk | Sulfur: Substitution Generation using a Logical Framework RocqPL Mathis Bouverot-Dupuis INRIA & École Normale Supérieure, Théo Winterhalter INRIA, Kenji Maillard Inria, Kathrin Stark Heriot-Watt University File Attached | ||