Program - POPL 2023

Detailed Table Session Timeline Detailed Timeline

Time Zone

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

Use conference time zone: (GMT-05:00) Eastern 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 21 Jan
Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30	Session 1CoqPL at Scollay

09:00 60m Talk		Omnisemantics: Smooth Handling of Nondeterminism (Invited talk) CoqPL Samuel Gruetter Massachusetts Institute of Technology
10:00 30m Talk		Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching CoqPL Xinyi Wan Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University File Attached

11:00 - 12:30	Session 2CoqPL at Scollay

11:00 30m Talk		Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation CoqPL Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Adam Chlipala Massachusetts Institute of Technology File Attached
11:30 30m Talk		Integrating graphical proofs in Coq CoqPL Pablo Donato Ecole polytechnique, Benjamin Werner LIX, IPP, Kaustuv Chaudhuri INRIA & LIX, IPP File Attached
12:00 30m Talk		Towards Formally Verified Path ORAM in Coq CoqPL Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign File Attached

14:00 - 15:30	Session 3CoqPL at Scollay

14:00 30m Talk		Verified Differential Privacy for Finite Computers CoqPL Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University File Attached
14:30 30m Talk		Formalizing Monoidal Categories and Actions for Syntax with Binders CoqPL Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft File Attached
15:00 30m Talk		Certifying Complexity Analysis CoqPL Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS File Attached

16:00 - 17:30	Session with the Coq development teamCoqPL at Scollay

16:00 45m Talk		Session with the Coq Development Team CoqPL Yves Bertot INRIA, Maxime Dénès Inria

CoqPL 2023 Program

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

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

CoqPL 2023 Program

Switch Program View

Program Display Configuration

Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change

Get Calendar (iCal)

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