POPL 2022 (series) / CoqPL 2022 (series) /
CoqPL 2022 Program
This is the CoqPL 2022 program - see the full program for POPL 2022 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote CoqPL |
10:20 - 12:00 | |||
10:20 20mTalk | A Visual Ltac Debugger in CoqIDERemote CoqPL File Attached | ||
10:40 20mTalk | Scrap your boilerplate definitions in 10 lines of Ltac!InPerson CoqPL File Attached | ||
11:00 20mTalk | 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 20mTalk | Towards a Formalization of Nominal Sets in CoqRemote CoqPL File Attached | ||
11:40 20mTalk | 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 | |||
13:30 60mKeynote | Verifying Concurrent, Crash-Safe Systems with PerennialRemote CoqPL |
14:30 - 14:50 | |||
14:30 20mTalk | 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 | |||
15:05 45mPanel | 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 |