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

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Invited Talk ICoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
09:00
60m
Keynote
Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote
CoqPL
10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntaxInPerson
CoqPL
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
13:30 - 14:30
Invited Talk IICoqPL at Salon I
Chair(s): Amin Timany Aarhus University
13:30
60m
Keynote
Verifying Concurrent, Crash-Safe Systems with PerennialRemote
CoqPL
I: Joseph Tassarotti Boston College
14:30 - 14:50
Contributed Talk (Afternoon)CoqPL at Salon I
Chair(s): Amin Timany Aarhus University
14:30
20m
Talk
A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote
CoqPL
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University
Pre-print File Attached
15:05 - 15:50
Session with the Coq Development TeamCoqPL at Salon I
Chair(s): Amin Timany Aarhus University
15:05
45m
Panel
Session with the Coq Development TeamRemote
CoqPL
S: Matthieu Sozeau Inria, S: Yves Bertot INRIA, S: Hugo Herbelin , S: Emilio Jesús Gallego Arias INRIA, S: Jason Gross MIT CSAIL