Program - POPL 2025

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT-07:00) Mountain Time (US & Canada).

Use conference time zone: (GMT-07:00) Mountain Time (US & Canada)Select 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

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30	Session 1CoqPL at Peek-A-Boo Chair(s): Kathrin Stark Heriot-Watt University

09:00 50m Keynote		Elpi: rule-based meta-languge for Rocq CoqPL Enrico Tassi INRIA Media Attached File Attached
09:50 20m Talk		Implementing OCaml APIs in Coq CoqPL Joshua M. Cohen Princeton University File Attached
10:10 20m Talk		Towards general white-box automation: a typeclass-guided context cleaner CoqPL Thibaut Pérami University of Cambridge File Attached

11:00 - 12:30	Session 2CoqPL at Peek-A-Boo Chair(s): Benjamin Delaware Purdue University

11:00 70m Panel		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria, Nicolas Tabareau Inria, Enrico Tassi INRIA, Yves Bertot INRIA
12:10 20m Talk		Vellvm: Formalizing the Informal CoqPL Calvin Beck University of Pennsylvania, USA, Hanxi Chen University of Pennsylvania, Steve Zdancewic University of Pennsylvania File Attached

14:00 - 15:30	Session 3CoqPL at Peek-A-Boo Chair(s): Benjamin Delaware Purdue University

14:00 22m Talk		Towards Verified Linear Algebra Programs Through Equivalence CoqPL Yihan Yang Harvey Mudd College, Mohit Tekriwal Lawrence Livermore National Laboratory, John Sarracino Lawrence Livermore National Laboratory, Matthew Sottile Lawrence Livermore National Laboratory, Ignacio Laguna Lawrence Livermore National Laboratory File Attached
14:22 22m Talk		A Framework of Differential Operators CoqPL Runqing Xu , Sebastian Erdweg JGU Mainz File Attached
14:45 22m Talk		A Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types CoqPL Tarakaram Gollamudi None, Jules Jacobs Cornell University, Yue Yao Carnegie Mellon University, Stephanie Balzer Carnegie Mellon University File Attached
15:07 22m Talk		Formal Verification of a Software Defined Delay-Tolerant Network CoqPL Jan-Paul Ramos-Davila Cornell University File Attached

16:00 - 17:30	Session 4 (16:00 - 17:30)CoqPL at Peek-A-Boo Chair(s): Qianchuan Ye University at Buffalo, SUNY

16:00 22m Talk		Towards Automated Verification of LLM-Synthesized C Programs CoqPL Prasita Mukherjee , Benjamin Delaware Purdue University File Attached
16:22 23m Talk		CoqNFU: Towards Formalizing NFU in Coq CoqPL Marko Doko Heriot-Watt University, UK, Vedran Čačić File Attached
16:45 22m Talk		Towards Mining Robust Coq Proof PatternsRemote Participation CoqPL Cezary Kaliszyk University of Melbourne, Xuan-Bach D. Le University of Melbourne, Christine Rizkallah University of Melbourne File Attached
17:07 22m Talk		Formal Verification of Quantum Stabilizer CodeRemote Participation CoqPL Qiuyi Feng , Udaya Parampalli , Christine Rizkallah University of Melbourne File Attached

CoqPL 2025 Program

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

CoqPL 2025 Program

Switch Program View

Program Display Configuration

Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change

Get Calendar (iCal)

Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change