Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" (RocqPL 2026 - Rocq for Programming Languages 2026)

Sun 11 - Sat 17 January 2026 Rennes, France

Who

Aria B. Eide, Vebjørn S. Øiestad, Mikhail Barash

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

Save

When

Sat 17 Jan 2026 17:00 - 17:15 at Salle 14 - Certified Programs and Proofs in Rocq

Abstract

We present an ongoing work on mechanizing the JavaScript’s feature proposal Temporal in the Rocq theorem prover. The proposal extends the standard library of JavaScript with functionality for working with dates, times, and calendars. Even with an incomplete mechanization, we identified several inconsistencies and points of improvement in the specification text of the proposal. Our findings were confirmed by one of the proposal champions, who has introduced modifications to the specification based on our input. Our work exemplifies benefits of a work-in-progress mechanization of a new feature in a major programming language.

File attachments

Extended Abstract (rocqpl26-final69.pdf)	421KiB

Aria B. Eide

University of Bergen

Vebjørn S. Øiestad

University of Bergen

Mikhail Barash

University of Bergen

Norway

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

Display full programSpecify a time band

Save

Session Program

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

16:00 - 18:00	Certified Programs and Proofs in RocqRocqPL at Salle 14

16:00 15m Talk		Abstract VCG: Tie-breaking rules in VCG mechanism design RocqPL Zhan JING Shanghai Jiao Tong University, Pierre Jouvelot
16:15 15m Talk		Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq RocqPL Harry Bryant Swansea University, Andrew Lawrence Siemens Mobility, Monika Seisenberger Swansea University, Anton Setzer Swansea University File Attached
16:30 15m Talk		Formalizing a First-order Differentiable Logic with MathComp RocqPL Jairo Miguel Marulanda-Giraldo University of Southampton
16:45 15m Talk		Recursive Mutexes in Separation Logic RocqPL Ke Du , William Mansky University of Illinois Chicago, Paolo G. Giarrusso Delft University of Technology, Gregory Malecha Skylabs AI
17:00 15m Talk		Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" RocqPL Aria B. Eide University of Bergen, Vebjørn S. Øiestad University of Bergen, Mikhail Barash University of Bergen File Attached
17:15 15m Talk		Verification of Templated Code in C++ RocqPL Gregory Malecha Skylabs AI, David Swasey Riverside Research, Simon Hudon SkyLabs AI
17:30 15m Talk		Lambda JS à la Carte RocqPL Kirill Golubev University of Turku, Mikhail Barash University of Bergen, Jaakko Järvi University of Turku File Attached

Hide past events