Dates
Tracks
Sun 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 60mTalk | Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant CPP Tobias NipkowTechnische Universität München Media Attached File Attached | ||
17:00 - 17:30 | Proof TacticsCPP at CPP Chair(s): Jesper CockxTU Delft Streamed session: https://youtu.be/PAxUO84tUE8?t=3781 | ||
17:00 15mTalk | A Novice-Friendly Induction Tactic for Lean CPP Jannis LimpergVrije Universiteit Amsterdam Pre-print Media Attached | ||
17:15 15mTalk | Lassie: HOL4 Tactics by Example CPP Heiko BeckerMPI-SWS, Nathaniel BosMcGill University, Ivan GavranMPI-SWS, Eva DarulovaMPI-SWS, Rupak MajumdarMPI-SWS Pre-print Media Attached File Attached | ||
18:00 - 18:45 | Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick ForsterSaarland University Streamed session: https://youtu.be/U_ZT9hfDAUQ | ||
18:00 15mTalk | An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier LaurentCNRS & 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 TimanyAarhus 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 SlagelNASA Langley Research Center, Lauren WhiteKansas State University, Aaron DutleNASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached | ||
Mon 18 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Andrei PopescuUniversity 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 SewellUniversity of Cambridge Media Attached | ||
17:00 - 17:30 | Program LogicsCPP at CPP Chair(s): William ManskyUniversity 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 BenzakenUniversité Paris Saclay, Sarah Cohen-BoulakiaLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne ContejeanCNRS, Chantal KellerLRI, Univ. Paris-Sud, Rébecca ZucchiniLRI, 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 HinrichsenIT University of Copenhagen, Daniël LouwrinkUniversity of Amsterdam, Robbert KrebbersRadboud University Nijmegen, Jesper BengtsonIT University of Copenhagen Pre-print Media Attached | ||
18:45 - 19:30 | Security, Blockchains, and Smart ContractsCPP at CPP Chair(s): Andreas LochbihlerDigital Asset Streamed session: https://youtu.be/Qak5mK92etU?t=2832 | ||
18:45 15mTalk | Extracting Smart Contracts Tested and Verified in Coq CPP Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Mikkel MiloConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium 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 MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity 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 ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State University Pre-print Media Attached | ||
20:00 - 21:00 | Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan ShankarSRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | ||
20:00 5mTalk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry RozplokhasSaint Petersburg State University and JetBrains Research, Andrey VyatkinSaint Petersburg State University, Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research Media Attached | ||
20:05 5mTalk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário PereiraNOVA LINCS & Nova School of Sciences and Tecnhology, Antonio RavaraDepartment 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-BertrandInria – LS2N, Université de Nantes, Kenji MaillardInria Nantes & University of Chile, Nicolas TabareauInria, Éric TanterUniversity of Chile Pre-print | ||
20:15 5mTalk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid JakobssonNomadic Labs, Colin GonzálezUniversité de Paris, Irif -- Nomadic Labs, Bruno BernardoNomadic Labs, Raphaël CauderlierNomadic Labs | ||
20:20 5mTalk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören BleikertzDigital Asset, Andreas LochbihlerDigital Asset, Ognjen MarićDigital Asset, Simon MeierDigital Asset, Phoebe NicholsDigital Asset, Matthias SchmalzDigital Asset, Ratko G. VeprekDigital 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 HolubCharles University, Štěpán StarostaFaculty 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 SidorencoAarhus University, Sabine OechsnerAarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University File Attached | ||
20:40 5mTalk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander KogtenkovSchaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
20:45 5mTalk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark WassellUniversity 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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 16:45 | Compilers and InterpretersCPP at CPP Chair(s): Freek WiedijkRadboud University Nijmegen Streamed session: https://youtu.be/TVqCuMMTuos | ||
16:00 15mTalk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. MyreenChalmers University of Technology Pre-print Media Attached | ||
16:15 15mTalk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas LööwChalmers University of Technology Pre-print Media Attached | ||
16:30 15mTalk | Towards Efficient and Verified Virtual Machines for Dynamic Languages CPP Martin DesharnaisUniversität der Bundeswehr München, Stefan BrunthalerUniversität der Bundeswehr München Pre-print Media Attached | ||
16:45 - 17:30 | Rewriting and Automated ReasoningCPP at CPP Chair(s): Cyril CohenUniversité 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 LochmannUniversity of Innsbruck, Aart MiddeldorpUniversity of Innsbruck, Fabian MitterwallnerUniversity of Innsbruck, Bertram Felgenhauer Pre-print Media Attached | ||
18:00 - 18:30 | AI and Machine LearningCPP at CPP Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK Streamed session: https://youtu.be/6NJdWdiZEiA | ||
18:00 15mTalk | A Formal Proof of PAC Learnability for Decision Stumps CPP Joseph TassarottiBoston College, Koundinya VajjhaUniversity of Pittsburgh, Anindya BanerjeeIMDEA Software Institute, Jean-Baptiste TristanBoston College Pre-print Media Attached | ||
18:15 15mTalk | CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq CPP Koundinya VajjhaUniversity of Pittsburgh, Avraham ShinnarIBM Research, Barry TragerIBM Research, Vasily PestunIBM Research; IHES, Nathan FultonIBM Research Pre-print Media Attached | ||
18:30 - 19:30 | |||
18:30 60mTalk | Chairs' report and community meeting CPP Media Attached File Attached | ||