Program - POPL 2024

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect 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

Sun 14 Jan
Displayed time zone: London change

10:30 - 11:00	BreakCatering at Maxwell Library

10:30 30m Coffee break		Break Catering

10:30 - 11:00	BreakCatering at Siemens Boardroom

10:30 30m Coffee break		Break Catering

12:30 - 14:00	LunchCatering at Maxwell Library

12:30 90m Lunch		Lunch Catering

12:30 - 14:00	LunchCatering at Siemens Boardroom

12:30 90m Lunch		Lunch Catering

15:30 - 16:00	BreakCatering at Maxwell Library

15:30 30m Coffee break		Break Catering

15:30 - 16:00	BreakCatering at Siemens Boardroom

15:30 30m Coffee break		Break Catering

Mon 15 Jan
Displayed time zone: London change

10:30 - 11:00	BreakCatering at Maxwell Library

10:30 30m Coffee break		Break Catering

12:30 - 14:00	LunchCatering at Maxwell Library

12:30 90m Lunch		Lunch Catering

15:30 - 16:00	BreakCatering at Maxwell Library

15:30 30m Coffee break		Break Catering

Tue 16 Jan
Displayed time zone: London change

	10:30 - 11:00	BreakCatering at Maxwell Library

10:30 - 11:00	BreakCatering at Riverside Room

10:30 30m Coffee break		Break Catering

12:30 - 14:00	LunchCatering at Maxwell Library

12:30 90m Lunch		Lunch Catering

12:30 - 14:00	LunchCatering at Riverside Room

12:30 90m Lunch		Lunch Catering

15:30 - 16:00	BreakCatering at Maxwell Library

15:30 30m Coffee break		Break Catering

15:30 - 16:00	BreakCatering at Riverside Room

15:30 30m Coffee break		Break Catering

Sat 20 Jan
Displayed time zone: London change

09:00 - 10:30	Session 1CoqPL at Kelvin Lecture

09:00 5m Day opening		Introduction CoqPL
09:05 60m Keynote		Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk) CoqPL I: Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria File Attached
10:05 25m Talk		CertiCoq-Wasm: Verified compilation from Coq to WebAssembly CoqPL Wolfgang Meier , Jean Pichon-Pharabod Aarhus University, Bas Spitters Aarhus University File Attached

10:30 - 11:00	BreakCatering at Maxwell Library

10:30 30m Coffee break		Break Catering

10:30 - 11:00	BreakCatering at Riverside Room

10:30 30m Coffee break		Break Catering

10:30 - 11:00	BreakCatering at Siemens Boardroom

10:30 30m Coffee break		Break Catering

11:00 - 12:30	Session 2CoqPL at Kelvin Lecture

11:00 90m Panel		Session with the Coq Development Team CoqPL Matthieu Sozeau Inria, Yves Bertot INRIA, Emilio Jesús Gallego Arias INRIA

12:30 - 14:00	LunchCatering at Maxwell Library

12:30 90m Lunch		Lunch Catering

	12:30 - 14:00	LunchCatering at Riverside Room

12:30 - 14:00	LunchCatering at Siemens Boardroom

12:30 90m Lunch		Lunch Catering

14:00 - 15:30	Session 3CoqPL at Kelvin Lecture

14:00 22m Talk		Well-founded recursion done right CoqPL Xavier Leroy Collège de France File Attached
14:22 22m Talk		Functorial Syntax for All CoqPL Filip Sieczkowski Heriot-Watt University, Piotr Polesiuk University of Wrocław File Attached
14:45 22m Talk		Specifying Smart Contract with Hax and ConCert CoqPL Lasse Letager Hansen Aarhus University, Bas Spitters Aarhus University File Attached
15:07 22m Talk		A formal security analysis of Blockchain voting CoqPL Nikolaj Sidorenco Aarhus University, Laura Brædder , Lasse Letager Hansen Aarhus University, Eske Hoy Nielsen Aarhus University, Bas Spitters Aarhus University File Attached

15:30 - 16:00	BreakCatering at Maxwell Library

15:30 30m Coffee break		Break Catering

15:30 - 16:00	BreakCatering at Riverside Room

15:30 30m Coffee break		Break Catering

15:30 - 16:00	BreakCatering at Siemens Boardroom

15:30 30m Coffee break		Break Catering

16:00 - 17:30	Session 4CoqPL at Kelvin Lecture

16:00 22m Talk		InducTeX: A MetaCoq plugin for typesetting inductive definitions CoqPL Jacco Krijnen Utrecht University File Attached
16:22 22m Talk		VsCoq 2, new foundations CoqPL Romain Tetley File Attached
16:45 22m Talk		Integrating Dependency Building with Document Checking in Coq CoqPL Emilio Jesús Gallego Arias INRIA, Bhakti Shah University of Chicago File Attached
17:07 22m Talk		A diagram editor to mechanize categorical proofs CoqPL Ambroise Lafont Ecole Polytechnique File Attached

CoqPL 2024 Program

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

CoqPL 2024 Program

Switch Program View

Program Display Configuration

Sun 14 JanDisplayed time zone: London change

Mon 15 JanDisplayed time zone: London change

Tue 16 JanDisplayed time zone: London change

Sat 20 JanDisplayed time zone: London change

Get Calendar (iCal)

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change