POPL 2024 (series) / CPP 2024 (series) /
CPP 2024 Program
This is the CPP 2024 program - see the full program for POPL 2024 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
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
09:00 - 10:30 | |||
09:00 60mKeynote | Under-approximation for Scalable Bug Detection CPP Azalea Raad Imperial College London | ||
10:00 30mTalk | A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic CPP Pre-print | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | Compiler / Program VerificationCPP at Kelvin Lecture Chair(s): Vadim Zaliva University of Cambridge, UK | ||
11:00 30mTalk | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography CPP Philipp G. Haselwarter Aarhus University, Benjamin Salling Hvass Aarhus University, Lasse Letager Hansen Aarhus University, Théo Winterhalter INRIA Saclay, Cătălin Hriţcu MPI-SP, Bas Spitters Aarhus University Pre-print File Attached | ||
11:30 30mTalk | UTC time, formally verified CPP Ana de Almeida Borges University of Barcelona and Formal Vindications S.L., Mireia González Bedmar University of Barcelona and Formal Vindications S.L., Juan Conejero Rodríguez University of Barcelona and Formal Vindications S.L., Eduardo Hermo Reyes University of Barcelona and Formal Vindications S.L., Joaquim Casals Buñuel University of Barcelona and Formal Vindications S.L., Joost J. Joosten University of Barcelona | ||
12:00 30mTalk | VCFloat2: Floating-point error analysis in Coq CPP Pre-print | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mTalk | A Temporal Differential Dynamic Logic Formal Embeddingremote presentation CPP | ||
14:30 30mTalk | Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemmadistinguished paper CPP Pre-print | ||
15:00 30mTalk | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs CPP Nao Hirokawa Japan Advanced Institute of Science and Technology, Dohan Kim University of Innsbruck, Kiraku Shintani Japan Advanced Institute of Science and Technology, René Thiemann University of Innsbruck | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||
16:00 - 17:30 | Formalizing MathematicsCPP at Kelvin Lecture Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota | ||
16:00 30mTalk | A Formalization of Complete Discrete Valuation Rings and Local Fields CPP María Inés de Frutos-Fernández Universidad Autónoma de Madrid, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio Université Jean Monnet Saint-Étienne Pre-print | ||
16:30 30mTalk | Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture CPP Siddhartha Gadgil Indian Institute of Science, Anand Rao Tadipatri Indian Institute of Science Education and Research | ||
17:00 30mTalk | Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Argumentsremote presentation CPP Joseph Eremondi University of Regina Pre-print | ||
17:35 - 18:30 | |||
17:35 55mMeeting | Business Meeting CPP | ||
Tue 16 JanDisplayed time zone: London change
Tue 16 Jan
Displayed time zone: London change
09:00 - 10:30 | |||
09:00 60mKeynote | Improved Assistance for Interactive Proof CPP Cezary Kaliszyk University of Innsbruck | ||
10:00 30mTalk | Martin-Löf à la Coqdistinguished paper CPP Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand University of Cambridge, Kenji Maillard INRIA, Pierre-Marie Pédrot INRIA, Loïc Pujet Stockholm University | ||
10:30 - 11:00 | |||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Catering | ||
11:00 - 12:30 | Formalizations of Category TheoryCPP at Kelvin Lecture Chair(s): Robert Atkey University of Strathclyde | ||
11:00 30mTalk | Displayed Monoidal Categories for the Semantics of Linear Logic CPP Benedikt Ahrens Delft University of Technology, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Niels van der Weide Radboud University, Kobe Wullaert Delft University of Technology | ||
11:30 30mTalk | Univalent Double Categories CPP Niels van der Weide Radboud University, Nima Rasekh Max Planck Institute for Mathematics, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University | ||
12:00 30mTalk | Formalizing the ∞-categorical Yoneda lemma CPP Nikolai Kudasov Innopolis University, Emily Riehl Johns Hopkins University, Jonathan Weinberger Johns Hopkins University Link to publication DOI Pre-print | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mTalk | Compositional Verification of Concurrent C Programs with Search Structure Templates CPP Duc-Than Nguyen University of Illinois at Chicago, Lennart Beringer Princeton University, William Mansky University of Illinois Chicago, Shengyi Wang Princeton University, USA Pre-print | ||
14:30 30mTalk | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logicdistinguished paper CPP Qiyuan Zhao National University of Singapore, George Pîrlea National University of Singapore, Zhendong Ang National University of Singapore, Umang Mathur National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
15:00 30mTalk | Unification for Subformula Linking under Quantifiers CPP Pre-print | ||
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 30mTalk | Lean Formalization of Extended Regular Expression Matching with Lookarounds CPP Ekaterina Zhuchko Tallinn University of Technology, Margus Veanes Microsoft Research, Gabriel Ebner Microsoft Research | ||
16:30 30mTalk | Memory simulations, security and optimization in a verified compiler CPP David Monniaux Université Grenoble Alpes - CNRS - Grenoble INP - Verimag | ||
17:00 30mTalk | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams CPP | ||
Sat 20 JanDisplayed time zone: London change
Sat 20 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 | ||
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 - 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 | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Catering | ||