Dates
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 17 Jan

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

08:50 - 09:00
Welcome from the chairsCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Talk
Coq’s vibrant ecosystem for verification engineeringInPerson
CPP
I: Andrew Appel Princeton
Link to publication
13:30 - 15:10
Semantics and Program VerificationCPP at Salon III
Chair(s): Benjamin Delaware Purdue University
13:30
25m
Talk
A Compositional Proof Framework for FRETish RequirementsRemote
CPP
Esther Conrad NASA LaRC, Laura Titolo NIA/NASA LaRC, Dimitra Giannakopoulou NASA Ames Research Center, Thomas Pressburger NASA ARC, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
13:55
25m
Talk
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with DerivativesRemote
CPP
Derek Egolf Northeastern University, Sam Lasser Tufts University, Kathleen Fisher Tufts University
Link to publication Media Attached
14:20
25m
Talk
Formally Verified Superblock SchedulingInPerson
CPP
Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Leo Gourdin Université Grenoble-Alpes, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Justus Fasse Université Grenoble-Alpes; KU Leuven, Nicolas Nardino École normale supérieure de Lyon
DOI Pre-print
14:45
25m
Talk
Overcoming Restraint: Composing Verification of Foreign Functions with CogentRemote
CPP
Louis Cheung University of Melbourne, Liam O'Connor University of Edinburgh, Christine Rizkallah University of Melbourne
DOI Pre-print Media Attached
15:30 - 17:10
Security and Distributed SystemsCPP at Salon III
Chair(s): Alwyn Goodloe NASA Langley Research Center
15:30
25m
Talk
Reflection, Rewinding, and Coin-Toss in EasyCryptRemote
CPP
Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu
Pre-print Media Attached
15:55
25m
Talk
A verified algebraic representation of Cairo program executionRemote
CPP
Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd.
Pre-print
16:20
25m
Talk
Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson
CPP
William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University
Pre-print
16:45
25m
Talk
Forward build systems, formallyInPerson
CPP
Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University
Link to publication
17:30 - 18:30
Invited TalkCPP at Salon III
Chair(s): Andrei Popescu University of Sheffield
17:30
60m
Talk
The seL4 verification: the art and craft of proof and the reality of commercial supportRemote
CPP
I: June Andronick Proofcraft, UNSW and seL4 Foundation
Media Attached

Tue 18 Jan

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

09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Laura Titolo NIA/NASA LaRC
09:00
60m
Talk
Structural Embeddings RevisitedRemote
CPP
10:20 - 12:00
Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
10:20
25m
Talk
CertiStr: A Certified String SolverDistinguished Paper AwardRemote
CPP
Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern
DOI Pre-print Media Attached
10:45
25m
Talk
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote
CPP
Michael Färber Universität Innsbruck, Austria
DOI Pre-print Media Attached File Attached
11:10
25m
Talk
An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote
CPP
Pre-print Media Attached
11:35
25m
Talk
A Drag-and-Drop Proof TacticRemote
CPP
Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique
DOI Pre-print Media Attached
15:30 - 16:10
Chairs' Report and Business MeetingCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntaxRemote
CPP
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University
DOI Pre-print Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTsRemote
CPP
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology
Pre-print Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theoryRemote
CPP
Jonathan Prieto-Cubides University of Bergen
Pre-print Media Attached
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote
CPP
Hing Lun Chan Australian National University
DOI Pre-print Media Attached File Attached