Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Room InformationNo extra information available
Program

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

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30
Proof TacticsCPP at CPP
Chair(s): Jesper CockxTU Delft

Streamed session: https://youtu.be/PAxUO84tUE8?t=3781

17:00
15m
Talk
A Novice-Friendly Induction Tactic for Lean
CPP
Jannis LimpergVrije Universiteit Amsterdam
Pre-print Media Attached
17:15
15m
Talk
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
15m
Talk
An Anti-Locally-Nameless Approach to Formalizing Quantifiers
CPP
Olivier LaurentCNRS & ENS Lyon
Pre-print Media Attached
18:15
15m
Talk
The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq
CPP
Dominik KirstSaarland University, Felix RechSaarland University
Pre-print Media Attached
18:30
15m
Talk
Formalizing Category Theory in Agda
CPP
Jason Z.S. HuMcGill University, Jacques CaretteMcMaster University
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
15m
Talk
Formalizing the Ring of Witt VectorsDistinguished Paper Award
CPP
Johan CommelinUniversität Freiburg, Robert Y. LewisVrije Universiteit Amsterdam
Pre-print Media Attached
19:00
15m
Talk
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
15m
Talk
On the Formalisation of Kolmogorov Complexity
CPP
Elliot CattANU, Michael NorrishData61, CSIRO & ANU
Pre-print Media Attached
20:00 - 21:00
Virtual CPP dinnerCPP at CPP

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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
15m
Talk
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
CPP
Simon Friis VindumAarhus University, Lars BirkedalAarhus University
Pre-print Media Attached
17:15
15m
Talk
Reasoning About Monotonicity in Separation Logic
CPP
Amin TimanyAarhus University, Lars BirkedalAarhus University
Pre-print Media Attached
18:00 - 18:45
SemanticsCPP at CPP
Chair(s): Yannick ZakowskiInria

Streamed session: https://youtu.be/Qak5mK92etU

18:00
15m
Talk
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
15m
Talk
Developing and certifying Datalog optimizations in Coq/MathComp
CPP
Pierre-Léo BégayOrange Labs & Verimag, Pierre CrégutOrange Labs, Jean-François MoninVerimag
Pre-print Media Attached
18:30
15m
Talk
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
15m
Talk
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
15m
Talk
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
15m
Talk
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
5m
Talk
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
5m
Talk
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
5m
Talk
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
5m
Talk
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
5m
Talk
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
5m
Talk
Specification and model checking of Tendermint consensus in TLA+
CPP Lightning Talks
Igor KonnovInformal Systems Inc, Zarko MilosevicInformal Systems, Josef WidderInformal Systems
20:30
5m
Talk
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
5m
Talk
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
5m
Talk
Mechanically-checked soundness of type-based null safety
CPP Lightning Talks
Alexander KogtenkovSchaffhausen Institute of Technology, Switzerland
Media Attached File Attached
20:45
5m
Talk
Formalising MiniSail in Isabelle
CPP Lightning Talks
Mark WassellUniversity of Cambridge
20:50
5m
Talk
How to verify an ASN.1 Protocol C-language Stack in Coq?
CPP Lightning Talks
Nika PonaDigamma.ai, Vadim ZalivaCarnegie 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
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
15m
Talk
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award
CPP
Magnus O. MyreenChalmers University of Technology
Pre-print Media Attached
16:15
15m
Talk
Lutsig: A Verified Verilog Compiler for Verified Circuit Development
CPP
Andreas LööwChalmers University of Technology
Pre-print Media Attached
16:30
15m
Talk
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
15m
Talk
A Modular Isabelle Framework for Verifying Saturation Provers
CPP
Sophie TourretMax Planck Institute for Informatics, Jasmin BlanchetteVrije 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. HaslbeckUniversity of Innsbruck, René ThiemannUniversity 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 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
15m
Talk
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
15m
Talk
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
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ţcuMPI-SP, Andrei PopescuUniversity of Sheffield, Lennart BeringerPrinceton University
Media Attached File Attached

Sun 17 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

Tue 19 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

Room16:0015304517:0015304518:0015304519:0015304520:00153045
CPP