POPL 2024 (series) / CoqPL 2024 (series) /
CoqPL 2024 Program
This is the CoqPL 2024 program - see the full program for POPL 2024 and all affiliated events.
Filter Program
Dates
Sun 14 Jan 2024
Mon 15 Jan 2024
Tue 16 Jan 2024
Sat 20 Jan 2024
Rooms
Kelvin Lecture
Maxwell Library
Riverside Room
Siemens Boardroom
Tracks
CoqPL
POPL Catering
Badges
Nothing to filter
Your Program
Nothing to filter
Sun 14 JanDisplayed time zone: London change
Sun 14 Jan
Displayed time zone: London change
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
Mon 15 JanDisplayed time zone: London change
Mon 15 Jan
Displayed time zone: London change
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
Tue 16 JanDisplayed time zone: London change
Tue 16 Jan
Displayed time zone: London change
10:30 - 11:00 | |||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
Sat 20 JanDisplayed time zone: London change
Sat 20 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 5mDay opening | Introduction CoqPL | ||
09:05 60mKeynote | Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk) CoqPL File Attached | ||
10:05 25mTalk | CertiCoq-Wasm: Verified compilation from Coq to WebAssembly CoqPL File Attached | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | |||
11:00 90mPanel | Session with the Coq Development Team CoqPL | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | Well-founded recursion done right CoqPL Xavier Leroy Collège de France File Attached | ||
14:22 22mTalk | Functorial Syntax for All CoqPL File Attached | ||
14:45 22mTalk | Specifying Smart Contract with Hax and ConCert CoqPL File Attached | ||
15:07 22mTalk | 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 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | |||
16:00 22mTalk | InducTeX: A MetaCoq plugin for typesetting inductive definitions CoqPL Jacco Krijnen Utrecht University File Attached | ||
16:22 22mTalk | VsCoq 2, new foundations CoqPL File Attached | ||
16:45 22mTalk | Integrating Dependency Building with Document Checking in Coq CoqPL File Attached | ||
17:07 22mTalk | A diagram editor to mechanize categorical proofs CoqPL Ambroise Lafont Ecole Polytechnique File Attached | ||