CPP

VenueOnline (How to POPL in 2021)

Room nameCPP

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

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 60m Talk		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 15m Talk		A Novice-Friendly Induction Tactic for Lean CPP Jannis Limperg Vrije Universiteit Amsterdam Pre-print Media Attached
17:15 15m Talk		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 15m Talk		An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier Laurent CNRS & ENS Lyon Pre-print Media Attached
18:15 15m Talk		The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq CPP Dominik Kirst Saarland University, Felix Rech Saarland University Pre-print Media Attached
18:30 15m Talk		Formalizing Category Theory in Agda CPP Jason Z.S. Hu McGill University, Jacques Carette McMaster University 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 15m Talk		Formalizing the Ring of Witt VectorsDistinguished Paper Award CPP Johan Commelin Universität Freiburg, Robert Y. Lewis Vrije Universiteit Amsterdam Pre-print Media Attached
19:00 15m Talk		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 15m Talk		On the Formalisation of Kolmogorov Complexity CPP Elliot Catt ANU, Michael Norrish Data61, CSIRO & ANU Pre-print Media Attached

	20:00 - 21:00	Virtual CPP dinnerCPP at CPP

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 60m Talk		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 15m Talk		Contextual Refinement of the Michael-Scott Queue (Proof Pearl) CPP Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University Pre-print Media Attached
17:15 15m Talk		Reasoning About Monotonicity in Separation Logic CPP Amin Timany Aarhus University, Lars Birkedal Aarhus University Pre-print Media Attached

18:00 - 18:45	SemanticsCPP at CPP Chair(s): Yannick Zakowski Inria Streamed session: https://youtu.be/Qak5mK92etU

18:00 15m Talk		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 15m Talk		Developing and certifying Datalog optimizations in Coq/MathComp CPP Pierre-Léo Bégay Orange Labs & Verimag, Pierre Crégut Orange Labs, Jean-François Monin Verimag Pre-print Media Attached
18:30 15m Talk		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 15m Talk		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 15m Talk		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 15m Talk		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 5m Talk		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 5m Talk		Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário Pereira NOVA LINCS & Nova School of Sciences and Tecnhology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
20:10 5m Talk		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 5m Talk		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 5m Talk		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 5m Talk		Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks Igor Konnov Informal Systems Inc, Zarko Milosevic Informal Systems, Josef Widder Informal Systems
20:30 5m Talk		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 5m Talk		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 5m Talk		Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander Kogtenkov Schaffhausen Institute of Technology, Switzerland Media Attached File Attached
20:45 5m Talk		Formalising MiniSail in Isabelle CPP Lightning Talks Mark Wassell University of Cambridge
20:50 5m Talk		How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks Nika Pona Digamma.ai, Vadim Zaliva Carnegie Mellon University, USA File Attached
20:55 5m Talk		Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias Kappé Cornell University

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 15m Talk		A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. Myreen Chalmers University of Technology Pre-print Media Attached
16:15 15m Talk		Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas Lööw Chalmers University of Technology Pre-print Media Attached
16:30 15m Talk		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 15m Talk		A Modular Isabelle Framework for Verifying Saturation Provers CPP Sophie Tourret Max Planck Institute for Informatics, Jasmin Blanchette Vrije Universiteit Amsterdam Pre-print Media Attached
17:00 15m Talk		An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR CPP Max W. Haslbeck University of Innsbruck, René Thiemann University of Innsbruck Pre-print Media Attached
17:15 15m Talk		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 15m Talk		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 15m Talk		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	Chairs' report and community meetingCPP at CPP Streamed session: https://youtu.be/6NJdWdiZEiA?t=2150

18:30 60m Talk		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

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00						30						17:00						30						18:00						30						19:00						30						20:00						30
CPP	CPP Invited Talk												CPP Proof Tactics												CPP Logic, Set Theory, and Category Theory									CPP Formalized Mathematics															CPP Virtual CPP dinner

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00						30						17:00						30						18:00						30						19:00						30						20:00						30
CPP	CPP Invited Talk												CPP Program Logics												CPP Semantics									CPP Security, Blockchains, and Smart Contracts															CPP + CPP Lightning Talks Lightning Talks

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00						30						17:00						30						18:00						30						19:00						30
CPP	CPP Compilers and Interpreters									CPP Rewriting and Automated Reasoning															CPP AI and Machine Learning						CPP Chairs' report and community meeting

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00			15			30			45			17:00			15			30			45			18:00			15			30			45			19:00			15			30			45
CPP	CPP Invited Talk: Teaching Algorithms and Data Structures with a Proof Assi ... 16:00 - 17:00												CPP A Novice-Friendly Induction Tactic for Lean 17:00 - 17:15			CPP Lassie: HOL4 Tactics by Example 17:15 - 17:30									CPP An Anti-Locally-Nameless Approach to Formalizing Quantifiers 18:00 - 18:15			CPP The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq 18:15 - 18:30			CPP Formalizing Category Theory in Agda 18:30 - 18:45			CPP Distinguished Paper Award Formalizing the Ring of Witt Vectors 18:45 - 19:00			CPP Formal Verification of Semi-algebraic Sets and Real Analytic Functions 19:00 - 19:15			CPP On the Formalisation of Kolmogorov Complexity 19:15 - 19:30

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00			15			30			45			17:00			15			30			45			18:00			15			30			45			19:00			15			30			45			20:00			15			30			45
CPP	CPP Invited Talk: Underpinning the foundations: Sail-based semantics, testi ... 16:00 - 17:00												CPP Contextual Refinement of the Michael-Scott Queue (Proof Pearl) 17:00 - 17:15			CPP Reasoning About Monotonicity in Separation Logic 17:15 - 17:30									CPP A Coq Formalization of Data Provenance 18:00 - 18:15			CPP Developing and certifying Datalog optimizations in Coq/MathComp 18:15 - 18:30			CPP Distinguished Paper Award Machine-Checked Semantic Session Typing 18:30 - 18:45			CPP Extracting Smart Contracts Tested and Verified in Coq 18:45 - 19:00			CPP Formal Verification of Authenticated, Append-Only Skip Lists in Agda 19:00 - 19:15			CPP Towards formally verified compilation of tag-based policy enforcement 19:15 - 19:30									CPP Lightning Talks Certified Semantics for miniKanren 20:00 - 20:05	CPP Lightning Talks Cameleer: a Deductive Verification Tool for OCaml 20:05 - 20:10	CPP Lightning Talks Gradualizing the Calculus of Inductive Constructions 20:10 - 20:15	CPP Lightning Talks Formally Verified Decentralized Exchange with Mi-Cho-Coq 20:15 - 20:20	CPP Lightning Talks A semantic domain for privacy-aware smart contracts and interoperable s ... 20:20 - 20:25	CPP Lightning Talks Specification and model checking of Tendermint consensus in TLA+ 20:25 - 20:30	CPP Lightning Talks Formalization of Combinatorics on Words in Isabelle/HOL 20:30 - 20:35	CPP Lightning Talks Formalising MPC-in-the-head-based zero-knowledge 20:35 - 20:40	CPP Lightning Talks Mechanically-checked soundness of type-based null safety 20:40 - 20:45	CPP Lightning Talks Formalising MiniSail in Isabelle 20:45 - 20:50	CPP Lightning Talks How to verify an ASN.1 Protocol C-language Stack in Coq? 20:50 - 20:55	CPP Lightning Talks Monadic Second-Order Logic and Pomset Languages 20:55 - 21:00

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change


Room	16:00			15			30			45			17:00			15			30			45			18:00			15			30			45			19:00			15			30			45
CPP	CPP Distinguished Paper Award A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) 16:00 - 16:15			CPP Lutsig: A Verified Verilog Compiler for Verified Circuit Development 16:15 - 16:30			CPP Towards Efficient and Verified Virtual Machines for Dynamic Languages 16:30 - 16:45			CPP A Modular Isabelle Framework for Verifying Saturation Provers 16:45 - 17:00			CPP An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR 17:00 - 17:15			CPP A Verified Decision Procedure for the First-Order Theory of Rewriting f ... 17:15 - 17:30									CPP A Formal Proof of PAC Learnability for Decision Stumps 18:00 - 18:15			CPP CertRL: Formalizing Convergence Proofs for Value and Policy Iteration i ... 18:15 - 18:30			CPP Chairs' report and community meeting 18:30 - 19:30

Room information: CPP

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

CPP + CPP Lightning Talks

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia

Room information: CPP

Program Display Configuration

Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

CPP

Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

CPP + CPP Lightning Talks

Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

CPP

CPP

CPP

CPP

Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change