ROCQWS — PROGRAM
Days: Saturday, 25 July 2026
Saturday, 25 July 2026
Location:
C6.08
| 09:00-10:00 |
Improving the Ring and Field tactics to ease mathematical learning (abstract) 60 min
1 Inria
|
Location:
C6.08
| 10:00-10:30 |
Towards Quantitative Logics in Rocq (abstract) 30 min
1 Heriot-Watt University
2 National Institute of Advanced Industrial Science and Technology (AIST)
3 IT-University of Copenhagen
4 University of Southampton and Heriot-Watt University
|
Location:
C6.08
| 11:00-11:30 |
Phantom Names: a Named Interface for de Bruijn Syntax (abstract) 30 min
1 Inria Paris
|
| 11:30-12:00 |
Sulfur: Automating Substitution-preserving Syntaxes and Judgments in Rocq (abstract) 30 min
1 ENS de Lyon
2 INRIA Paris, ENS Paris
3 INRIA Rennes
4 Université Paris-Saclay, INRIA, CNRS, ENS Paris-Saclay, LMF
|
| 12:00-12:30 |
A Category of Finite Ordinals and Functions with Computable Pullbacks and Pushouts in Rocq (abstract) 30 min
1 ENS de Lyon
|
Location:
C6.08
| 14:00-14:30 |
40 years of Guard Conditions (abstract) 30 min
1 Nantes Université, Inria
2 Inria
3 KU Leuven
|
| 14:30-15:00 |
Camltac: OCaml as a Tactic Language (abstract) 30 min
1 EPFL
|
| 15:00-15:30 |
Towards Robust Programming Interfaces in Rocq (abstract) 30 min
1 ENS de Lyon & Eötvös Loránd University
|
Location:
C6.08
| 16:00-16:30 |
An Attempt at Necromancy – Experience Report on Modernising a Domain Theory Library (abstract) 30 min
1 INRIA
|
| 16:30-17:00 |
Certified JSON Derivers with ELPI (abstract) 30 min
1 University of Kansas
|