Dates
Tracks
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Cătălin Hriţcu MPI-SP Streamed session: https://youtu.be/PAxUO84tUE8 | ||
16:00 60mTalk | Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant CPP Tobias Nipkow Technische Universität München Media Attached File Attached | ||
17:00 - 17:30 | Proof TacticsCPP at CPP Chair(s): Jesper Cockx TU Delft Streamed session: https://youtu.be/PAxUO84tUE8?t=3781 | ||
17:00 15mTalk | A Novice-Friendly Induction Tactic for Lean CPP Jannis Limperg Vrije Universiteit Amsterdam Pre-print Media Attached | ||
17:15 15mTalk | Lassie: HOL4 Tactics by Example CPP Heiko Becker MPI-SWS, Nathaniel Bos McGill University, Ivan Gavran MPI-SWS, Eva Darulova MPI-SWS, Rupak Majumdar MPI-SWS Pre-print Media Attached File Attached | ||
18:00 - 18:45 | Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick Forster Saarland University Streamed session: https://youtu.be/U_ZT9hfDAUQ | ||
18:00 15mTalk | An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier Laurent CNRS & ENS Lyon Pre-print Media Attached | ||
18:15 15mTalk | The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq CPP Pre-print Media Attached | ||
18:30 15mTalk | Formalizing Category Theory in Agda CPP Pre-print Media Attached | ||
18:45 - 19:30 | Formalized MathematicsCPP at CPP Chair(s): Amin Timany Aarhus University Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768 | ||
18:45 15mTalk | Formalizing the Ring of Witt VectorsDistinguished Paper Award CPP Pre-print Media Attached | ||
19:00 15mTalk | Formal Verification of Semi-algebraic Sets and Real Analytic Functions CPP J Tanner Slagel NASA Langley Research Center, Lauren White Kansas State University, Aaron Dutle NASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached | ||
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Andrei Popescu University of Sheffield Streamed session: https://youtu.be/poHYVOMQuro?t=144 | ||
16:00 60mTalk | Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures CPP Peter Sewell University of Cambridge Media Attached | ||
17:00 - 17:30 | Program LogicsCPP at CPP Chair(s): William Mansky University of Illinois at Chicago Streamed session: https://youtu.be/poHYVOMQuro?t=3869 | ||
17:00 15mTalk | Contextual Refinement of the Michael-Scott Queue (Proof Pearl) CPP Pre-print Media Attached | ||
17:15 15mTalk | Reasoning About Monotonicity in Separation Logic CPP Pre-print Media Attached | ||
18:00 - 18:45 | |||
18:00 15mTalk | A Coq Formalization of Data Provenance CPP Véronique Benzaken Université Paris Saclay, Sarah Cohen-Boulakia LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne Contejean CNRS, Chantal Keller LRI, Univ. Paris-Sud, Rébecca Zucchini LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay Pre-print Media Attached | ||
18:15 15mTalk | Developing and certifying Datalog optimizations in Coq/MathComp CPP Pre-print Media Attached | ||
18:30 15mTalk | Machine-Checked Semantic Session TypingDistinguished Paper Award CPP Jonas Kastberg Hinrichsen IT University of Copenhagen, Daniël Louwrink University of Amsterdam, Robbert Krebbers Radboud University Nijmegen, Jesper Bengtson IT University of Copenhagen Pre-print Media Attached | ||
18:45 - 19:30 | Security, Blockchains, and Smart ContractsCPP at CPP Chair(s): Andreas Lochbihler Digital Asset Streamed session: https://youtu.be/Qak5mK92etU?t=2832 | ||
18:45 15mTalk | Extracting Smart Contracts Tested and Verified in Coq CPP Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University Pre-print Media Attached File Attached | ||
19:00 15mTalk | Formal Verification of Authenticated, Append-Only Skip Lists in Agda CPP Victor Cacciari Miraldo DFINITY Foundation, Harold Carr Oracle Labs, USA, Mark Moir Oracle Labs, New Zealand, Lisandra Silva University of Minho, Guy L. Steele Jr. Oracle Labs Pre-print Media Attached | ||
19:15 15mTalk | Towards formally verified compilation of tag-based policy enforcement CPP CHR Chhak Portland State University, Andrew Tolmach Portland State University, Sean Anderson Portland State University Pre-print Media Attached | ||
20:00 - 21:00 | Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan Shankar SRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | ||
20:00 5mTalk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry Rozplokhas Saint Petersburg State University and JetBrains Research, Andrey Vyatkin Saint Petersburg State University, Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research Media Attached | ||
20:05 5mTalk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário Pereira NOVA LINCS & Nova School of Sciences and Tecnhology, Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
20:10 5mTalk | Gradualizing the Calculus of Inductive Constructions CPP Lightning Talks Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile Pre-print | ||
20:15 5mTalk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid Jakobsson Nomadic Labs, Colin González Université de Paris, Irif -- Nomadic Labs, Bruno Bernardo Nomadic Labs, Raphaël Cauderlier Nomadic Labs | ||
20:20 5mTalk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören Bleikertz Digital Asset, Andreas Lochbihler Digital Asset, Ognjen Marić Digital Asset, Simon Meier Digital Asset, Phoebe Nichols Digital Asset, Matthias Schmalz Digital Asset, Ratko G. Veprek Digital Asset File Attached | ||
20:25 5mTalk | Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks | ||
20:30 5mTalk | Formalization of Combinatorics on Words in Isabelle/HOL CPP Lightning Talks Štěpán Holub Charles University, Štěpán Starosta Faculty of Information Technology, Czech Technical University in Prague Link to publication Media Attached File Attached | ||
20:35 5mTalk | Formalising MPC-in-the-head-based zero-knowledge CPP Lightning Talks Nikolaj Sidorenco Aarhus University, Sabine Oechsner Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University File Attached | ||
20:40 5mTalk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander Kogtenkov Schaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
20:45 5mTalk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark Wassell University of Cambridge | ||
20:50 5mTalk | How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks File Attached | ||
20:55 5mTalk | Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias Kappé Cornell University | ||
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 16:45 | Compilers and InterpretersCPP at CPP Chair(s): Freek Wiedijk Radboud University Nijmegen Streamed session: https://youtu.be/TVqCuMMTuos | ||
16:00 15mTalk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. Myreen Chalmers University of Technology Pre-print Media Attached | ||
16:15 15mTalk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas Lööw Chalmers University of Technology Pre-print Media Attached | ||
16:30 15mTalk | Towards Efficient and Verified Virtual Machines for Dynamic Languages CPP Martin Desharnais Universität der Bundeswehr München, Stefan Brunthaler Universität der Bundeswehr München Pre-print Media Attached | ||
16:45 - 17:30 | Rewriting and Automated ReasoningCPP at CPP Chair(s): Cyril Cohen Université Côte d’Azur, Inria, France Streamed session: https://youtu.be/TVqCuMMTuos?t=2806 | ||
16:45 15mTalk | A Modular Isabelle Framework for Verifying Saturation Provers CPP Pre-print Media Attached | ||
17:00 15mTalk | An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR CPP Pre-print Media Attached | ||
17:15 15mTalk | A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems CPP Alexander Lochmann University of Innsbruck, Aart Middeldorp University of Innsbruck, Fabian Mitterwallner University of Innsbruck, Bertram Felgenhauer Pre-print Media Attached | ||
18:00 - 18:30 | AI and Machine LearningCPP at CPP Chair(s): Ekaterina Komendantskaya Heriot-Watt University, UK Streamed session: https://youtu.be/6NJdWdiZEiA | ||
18:00 15mTalk | A Formal Proof of PAC Learnability for Decision Stumps CPP Joseph Tassarotti Boston College, Koundinya Vajjha University of Pittsburgh, Anindya Banerjee IMDEA Software Institute, Jean-Baptiste Tristan Boston College Pre-print Media Attached | ||
18:15 15mTalk | CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq CPP Koundinya Vajjha University of Pittsburgh, Avraham Shinnar IBM Research, Barry Trager IBM Research, Vasily Pestun IBM Research; IHES, Nathan Fulton IBM Research Pre-print Media Attached | ||
18:30 - 19:30 | |||
18:30 60mTalk | Chairs' report and community meeting CPP Cătălin Hriţcu MPI-SP, Andrei Popescu University of Sheffield, Lennart Beringer Princeton University Media Attached File Attached | ||