Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online

Conference Dates
Conference Dates are in time zone (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna, and may differ from the viewed time zone.
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

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

07:00 - 08:00
07:00
60m
Social Event
POPL Card Game
POPL Meetups
15:30 - 16:00
15:30
30m
Social Event
Sunday Breakfast Tables
Workshops and Co-located Events
16:00 - 16:50
Invited talk: Vikash K. MansinghkaLAFI at LAFI
Chair(s): Jean-Baptiste TristanBoston College
16:00 - 17:30
Secure compilers & cryptographyPriSC at PriSC
Chair(s): Fraser BrownStanford University, USA, Aastha MehtaMPI-SWS, Germany and University of British Columbia, Canada
16:00
18m
Talk
High-level high-speed high-assurance crypto
PriSC
Jonathan CoganStanford, Fraser BrownStanford University, USA, Alex OzdemirStanford, Riad S. WahbyStanford University, USA
Media Attached
16:18
18m
Talk
Cross-Architecture Testing for Compiler-Introduced Security Bugs
PriSC
Jianhao XuNanjing University, Kangjie LuUniversity of Minnesota, Bing MaoNanjing University
Media Attached File Attached
16:36
18m
Talk
High-Assurance Cryptography in the Spectre Era
PriSC
Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Sunjay CauligiUniversity of California at San Diego, USA, Benjamin GregoireINRIA, Adrien KoutsosINRIA Paris, Kevin LiaoMax Planck Institute for Security and Privacy, Tiago OliveiraUniversity of Porto (FCUP) and INESC TEC, Swarn PriyaPurdue University, Tamara RezkInria, France, Peter SchwabeMax Planck Institute for Security and Privacy
Media Attached
16:54
18m
Talk
Compilation as Multi-Language Semantics
PriSC
William J. BowmanUniversity of British Columbia
Pre-print Media Attached
17:12
18m
Talk
Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
PriSC
Coşku AcayCornell University, Rolph Recto, Joshua GancherCornell University, Andrew C. MyersCornell University, Elaine ShiCornell University
Media Attached
16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir VizelTechnion—Israel Institute of Technology
16:00
60m
Keynote
Model Checking Hyperproperties
VMCAI
I: Bernd FinkbeinerCISPA Helmholtz Center for Information Security
Media Attached
16:50 - 17:30
Session 1LAFI at LAFI
Chair(s): Jean-Baptiste TristanBoston College
16:50
13m
Talk
Binary Tree Hamiltonian Monte Carlo
LAFI
Carol MakUniversity of Oxford, Fabian ZaiserUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
File Attached
17:03
13m
Talk
An algebraic theory of conditioning
LAFI
Dario SteinUniversity of Oxford, Sam StatonUniversity of Oxford
File Attached
17:16
13m
Talk
The Selection Monad and Decision-Making Languages
LAFI
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
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
17:00 - 17:30
HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory FedyukovichFlorida State University
17:00
15m
Talk
Compositional Model Checking for Multi-Properties
VMCAI
Ohad GoudsmidDepartment of Computer Science, The Technion, Orna GrumbergTechnion – Israel Institute of Technology, Sarai SheinvaldDepartment of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15
15m
Talk
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Eric KoskinenStevens Institute of Technology, Kshitij BansalGoogle
Media Attached
17:30 - 18:00
17:30
30m
Break
Sunday Coffee Break
Workshops and Co-located Events
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:00 - 19:30
Session 2LAFI at LAFI
Chair(s): Dougal MaclaurinGoogle Research
18:00
12m
Talk
Enzyme: High-Performance Automatic Differentiation of LLVM
LAFI
William S. MosesMassachusetts Institute of Technology, Valentin ChuravyMIT CSAIL
18:12
12m
Talk
Parametric Inversion of Non-Invertible Programs
LAFI
Zenna TavaresMassachusetts Institute of Technology, Javier BurroniUniversity of Massachusetts Amherst, Edgar MinasyanPrinceton University, David MorejonMassachusetts Institute of Technology, Armando Solar-LezamaMassachusetts Institute of Technology
File Attached
18:25
12m
Talk
Bayesian Neural Ordinary Differential Equations
LAFI
Raj DandekarMIT, Vaibhav DixitJulia Computing, Mohamed TarekUNSW Canberra, Australia, Aslan Garcia ValadezNational Autonomous University of Mexico, Chris RackauckasMIT
Pre-print Media Attached File Attached
18:38
12m
Talk
On the Automatic Derivation of Importance Samplers from Pairs of Probabilistic Programs
LAFI
Alexander K. LewMassachusetts Institute of Technology, USA, Ben Sherman, Marco Cusumano-TownerMIT-CSAIL, Michael CarbinMassachusetts Institute of Technology, Vikash K. MansinghkaMIT
Media Attached
18:51
12m
Talk
Decomposing reverse-mode automatic differentiation
LAFI
Roy FrostigGoogle Research, Matthew JohnsonGoogle Brain, Dougal MaclaurinGoogle Research, Adam PaszkeGoogle Research, Alexey RadulGoogle Research
File Attached
19:04
12m
Talk
Genify.jl: Transforming Julia into Gen to enable programmable inference
LAFI
Tan Zhi-XuanMassachusetts Institute of Technology, McCoy R. BeckerCharles River Analytics, Vikash K. MansinghkaMIT
Media Attached File Attached
19:17
12m
Talk
Probabilistic Inference Using Generators: the Statues Algorithm
LAFI
Pierre Denisindependent scholar
Link to publication DOI Pre-print Media Attached File Attached
18:00 - 19:00
Invited talkPriSC at PriSC
Chair(s): Deian StefanUniversity of California at San Diego, USA
18:00
60m
Keynote
Frontiers in Secure Compilation – an Industrial Perspective (invited talk)
PriSC
Hugo VincentArm Research
18:00 - 19:30
18:00
90m
Poster
SRC Poster Session
Student Research Competition
18:00 - 18:30
Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna GrumbergTechnion – Israel Institute of Technology
18:00
15m
Talk
Proving the existence of fair paths in infinite state systems
VMCAI
Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler
Media Attached
18:15
15m
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar NamjoshiNokia Bell Labs, Anton XueUniversity of Pennsylvania
Media Attached
18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler CohenTechnion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina PetersonUniversity of Central Florida, Victor CookUniversity of Central Florida, Damian DechevUniversity of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel DietschUniversity of Freiburg, Matthias HeizmannUniversity of Freiburg, Germany, Dominik KlumppUniversity of Freiburg, Mehdi NaouarUniversity of Freiburg, Andreas PodelskiUniversity of Freiburg, Germany, Claus SchätzleUniversity of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina StoilkovskaVienna University of Technology , Igor KonnovInformal Systems Inc, Josef WidderInformal Systems, Florian ZulegerVienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie BertrandINRIA Rennes, Marijana LazicTechnical University of Munich, Josef WidderInformal Systems
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
19:00 - 20:30
Formal analysis & proof techniquesPriSC at PriSC
Chair(s): Marco PatrignaniStanford University, USA / CISPA, Germany, Jonathan ProtzenkoMicrosoft Research, Redmond
19:00
18m
Talk
Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
PriSC
Pre-print Media Attached
19:18
18m
Talk
Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
PriSC
Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH
Media Attached
19:36
18m
Talk
Secure Optimization Through Opaque Observations
PriSC
Son Tuan VuSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert CohenGoogle, Karine HeydemannSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Arnaud de GrandmaisonARM, Christophe GuillonSTMicroelectronics
Pre-print Media Attached File Attached
19:54
18m
Talk
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine AbateMax Planck Institute for Security and Privacy, Bochum, Germany, Matteo BusiUniversità di Pisa - Dipartimento di Informatica
Pre-print Media Attached File Attached
20:12
18m
Talk
Toward Complete Stack Safety for Capability Machines
PriSC
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached File Attached
19:30 - 20:00
19:30
30m
Social Event
Sunday Hallway Time
Workshops and Co-located Events
20:00 - 21:00
Virtual CPP dinnerCPP at CPP
21:00 - 21:30
Short talksPriSC at PriSC
Chair(s): Deian StefanUniversity of California at San Diego, USA
21:00
15m
Talk
A Categorical Approach to Secure Compilation (and others things) (short talk)
PriSC
Stylianos Tsampas, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel, Frank PiessensKU Leuven
21:15
15m
Talk
Contract-aware Secure Compilation (short talk)
PriSC
Marco GuarnieriETH Zurich, Switzerland, Marco PatrignaniStanford University, USA / CISPA, Germany
Pre-print

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

04:30 - 05:30
04:30
60m
Social Event
Panel Discussion 1: Choosing Research Topics
POPL Meetups
Chung-Kil HurSeoul National University, South Korea, Christine RizkallahUNSW Sydney, Hongseok YangKAIST, Ilya SergeyYale-NUS College and National University of Singapore, James NobleVictoria University of Wellington
07:00 - 08:00
07:00
60m
Break
Monday Coffee Break 1
POPL Meetups
10:00 - 11:00
Session 1PEPM at PEPM
Chair(s): Torben MogensenDIKU, University of Copenhagen

Live stream: https://www.youtube.com/watch?v=fvWxWyV05v4

10:00
30m
Short-paper
A Functional Abstraction of Typed Trails
PEPM
Kenichi AsaiOchanomizu University, Youyou CongTokyo Institute of Technology, Chiaki IshioOchanomizu University
Media Attached File Attached
10:30
30m
Research paper
A Text-based Syntax Completion Method Using LR Parsing
PEPM
Isao SasanoShibaura Institute of Technology, Kwanghoon ChoiChonnam National University
Media Attached
11:30 - 12:30
Session 2PEPM at PEPM
Chair(s): Youyou CongTokyo Institute of Technology

Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM

11:30
30m
Research paper
Coq to C Translation with Partial Evaluation
PEPM
Akira TanakaNational Institute of Advanced Industrial Science and Technology (AIST)
Media Attached
12:00
30m
Research paper
Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award
PEPM
Hideto UenoThe Univeristy of Tokyo, John TomanCertora, inc., Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, Japan
Media Attached
13:30 - 14:30
Session 3PEPM at PEPM
Chair(s): Robert AtkeyUniversity of Strathclyde

Live stream: https://www.youtube.com/watch?v=G5vngBBn398

13:30
30m
Short-paper
Control Flow Obfuscation for Featherweight Java using Continuation Passing
PEPM
Kenny Zhuo Ming LuISTD, Singapore University of Technology and Design
Media Attached File Attached
14:00
30m
Research paper
Efficient Fair Conjunction for Structurally-Recursive Relations
PEPM
Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research
Media Attached File Attached
14:30 - 15:30
Keynote 1PADL at PADL
Chair(s): Dominic OrchardUniversity of Kent, UK
14:30
60m
Keynote
Semantics-based Synthesis in miniKanren
PADL
William E. ByrdUniversity of Alabama at Birmingham, USA
14:30 - 15:15
Session 0PLMW at PLMW
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
14:30
45m
Talk
Think Abstractly, Work Concretely
PLMW
Ichiro HasuoNational Institute of Informatics, Japan
Media Attached
15:00 - 16:00
Keynote 1PEPM at PEPM
Chair(s): Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK

Live stream: https://www.youtube.com/watch?v=kaJOj_LErQo

The PEPM 2021 Best Paper Award will be announced at the beginning of this session immediately before this keynote.

15:00
60m
Keynote
Program Manipulation of C Code: From Partial Evaluation to Semantic Patches for the Linux Kernel
PEPM
File Attached
15:30 - 16:00
15:30
30m
Social Event
Topic Oriented Discussions
Workshops and Co-located Events
16:00 - 17:30
Applications of Declarative LanguagesPADL at PADL
Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK
16:00
30m
Research paper
A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
PADL
Fabio TardivoNew Mexico State University, Loc PhamNew Mexico State University, Tran Cao SonNew Mexico State University, Enrico PontelliNew Mexico State University
16:30
30m
Research paper
Data validation meets Answer Set Programming
PADL
Mario AlvianoUniversity of Calabria, Carmine DodaroDepartment of Mathematics and Computer Science, University of Calabria, Arnel ZamaylaUniversity of Calabria, Italy
17:00
30m
Research paper
Lightweight Declarative Server-Side Web Programming
PADL
Michael HanusKiel University
16:00 - 17:30
Session 1PLMW at PLMW
Chair(s): Azalea RaadImperial College London
16:00
45m
Talk
Numbers, Logic, and Decidability Results for Cyber-Physical Systems
PLMW
16:45
45m
Talk
The Lean Researcher
PLMW
Alastair F. DonaldsonImperial College London and Google
16:00 - 17:30
16:00
90m
Tutorial
[T1] The Current State of Automatic Differentiation
TutorialFest
Barak A. PearlmutterMaynooth University
16:00 - 17:30
16:00
90m
Tutorial
[T2] Liquid Haskell: Refinement Type Checker for Haskell
TutorialFest
Niki VazouIMDEA Software Institute, Andres LöhWell-Typed LLP
16:00 - 17:30
16:00
90m
Tutorial
[T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice
TutorialFest
Umang MathurUniversity of Illinois at Urbana-Champaign, Andreas PavlogiannisAarhus University
Pre-print Media Attached File Attached
16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir VizelTechnion—Israel Institute of Technology
16:00
60m
Keynote
Algebra-based Synthesis of Loops and their Invariants
VMCAI
I: Laura KovacsVienna University of Technology (TU Wien), Andreas HumenbergerVienna University of Technology
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
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
17:00 - 17:30
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
17:00
15m
Talk
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Franck VédrineCEA LIST, Maxime JacqueminCEA LIST, France, Nikolai KosmatovThales Research and Technology, Julien SignolesCEA LIST
Media Attached
17:15
15m
Talk
Twinning automata and regular expressions for string static analysis
VMCAI
Luca NegriniCa’ Foscari University of Venice, Julia S.r.l., Vincenzo ArceriCa’ Foscari University of Venice, Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia
Media Attached
17:30 - 18:00
17:30
30m
Break
Monday Coffee Break 2
Workshops and Co-located Events
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:00 - 19:30
Foundations and Programming ConceptsPADL at PADL
Chair(s): Dominic OrchardUniversity of Kent, UK
18:00
30m
Research paper
A Family of Unification-oblivious Program Transformations and Their Applications
PADL
Paul TarauUniversity of North Texas
18:30
30m
Research paper
On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages
PADL
David YoungUniversity of Kansas, USA, Mark GrebeUniversity of Central Missouri, USA, Andy GillUniversity of Kansas, USA
18:00 - 19:30
18:00
90m
Tutorial
[T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic
TutorialFest
Tej ChajedMassachusetts Institute of Technology, USA, Ralf JungMPI-SWS, Joseph TassarottiBoston College
Link to publication
18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. WilcoxUniversity of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren PickPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University
Media Attached
18:15
15m
Talk
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Hongce ZhangPrinceton University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
Media Attached
18:30 - 19:15
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison, USA
18:30
15m
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius KampFriedrich-Alexander University Erlangen-Nürnberg, Michael PhilippsenFriedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45
15m
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan NguyenNational University of Singapore, Quang-Trung TaNational University of Singapore, Ilya SergeyYale-NUS College and National University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
19:00
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh JoshiIIT Hyderabad, Gautam MudugantiIIT Hyderabad
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
19:30 - 20:00
19:30
30m
Social Event
Monday Shuffle-Space Time
Workshops and Co-located Events
20:00 - 21:00
20:00
60m
Social Event
POPL Card Game
Workshops and Co-located Events
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
20:00 - 21:00
Monday PanelPLMW at PLMW
Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA
20:00
60m
Live Q&A
Panel: Doing Research in PL
PLMW
Greg MorrisettCornell Tech, Susan EisenbachImperial College London, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, Jeehoon KangKAIST, Delphine DemangeUniv Rennes, Inria, CNRS, IRISA, Kuen-Bang Hou (Favonia)University of Minnesota, Twin Cities

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

04:30 - 05:30
04:30
60m
Social Event
Panel Discussion 2: Improving Peer Review
POPL Meetups
Hongseok YangKAIST, Ilya SergeyYale-NUS College and National University of Singapore, James NobleVictoria University of Wellington, Soham ChakrabortyIIT Delhi, India, Youyou CongTokyo Institute of Technology
07:00 - 08:00
07:00
60m
Break
Tuesday Coffee Break 1
POPL Meetups
14:30 - 15:30
Invited TalkCoqPL at CoqPL
14:30
60m
Keynote
Verifying a compiler through equational means
CoqPL
14:30 - 15:30
Keynote 2PADL at PADL
Chair(s): José MoralesIMDEA Software Institute
14:30
60m
Keynote
SMT-based Constraint Answer Set Solver EZSMT
PADL
Yuliya LierlerUniversity of Nebraska
14:30 - 15:30
Tuesday PanelPLMW at PLMW
Chair(s): Stephanie BalzerCarnegie Mellon University, USA
14:30
60m
Live Q&A
Panel: Navigating PhD studies
PLMW
Hila PelegUniversity of California at San Diego, Nick GiannarakisUniversity of Wisconsin-Madison, Anne-Kathrin SchmuckMPI-SWS, Sacha-Élie AyounImperial College London, Farzaneh DerakhshanCarnegie Mellon University, Soham ChakrabortyIIT Delhi
15:00 - 16:00
Keynote 2PEPM at PEPM
Chair(s): Torben MogensenDIKU, University of Copenhagen

Live stream: https://www.youtube.com/watch?v=Ps_rUSG1yg0

15:00
60m
Keynote
Erasure In Dependently Typed Programming
PEPM
15:30 - 16:00
15:30
30m
Social Event
Tuesday Shuffle-Space Time
Workshops and Co-located Events
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:00 - 17:30
Contributed TalksCoqPL at CoqPL
16:00
15m
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason GrossMIT CSAIL
Media Attached File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui QiNagoya University, Jacques GarrigueNagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej ChajedMassachusetts Institute of Technology, USA
Media Attached File Attached
16:45
15m
Break
Break
CoqPL
17:00
15m
Talk
The B+-tree Index as a Verified Software Unit
CoqPL
Anastasiya Kravchuk-KirilyukHarvard University, Andrew AppelPrinceton, Lennart BeringerPrinceton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul ChiplunkarMassachusetts Institute of Technology, Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology
File Attached
16:00 - 17:30
Declarative Approaches to Testing and DebuggingPADL at PADL
Chair(s): Paul TarauUniversity of North Texas
16:00
30m
Research paper
ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs
PADL
Sumit PadhiyarIndian Institue Of Technology, Madras, KC SivaramakrishnanIIT Madras
Link to publication
16:30
30m
Research paper
Causal-Consistent Reversible Debugging: Improving CauDEr
PADL
Juan José González-AbrilMiST, VRAIN, Universitat Politecnica de Valencia, German VidalUniversitat Politecnica de Valencia
17:00
30m
Research paper
Declarative Debugging of XML Queries
PADL
Jesus M. Almendros-JimenezUniversidad de Almeria, Antonio Becerra-TeronUniversity of Almeria
16:00 - 17:30
Session 3PLMW at PLMW
Chair(s): Azalea RaadImperial College London
16:00
45m
Talk
Connecting Information Flow Types to Runtime Monitors via Gradual Typing
PLMW
Limin JiaCarnegie Mellon University
16:45
45m
Talk
Emotional Machines
PLMW
16:00 - 17:00
Invited talkVMCAI at VMCAI
16:00
60m
Keynote
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
VMCAI
I: Bernhard SteffenTU Dortmund, Alnis MurtoviTU Dortmund, David SchmidtKansas State University
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
17:00 - 17:30
ApplicationsVMCAI at VMCAI
Chair(s): Rayna DimitrovaCISPA Helmholtz Center for Information Security
17:00
15m
Talk
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Yahui SongNational University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
17:15
15m
Talk
A Design of GPU-Based Quantitative Model Checking
VMCAI
YoungMin KwonSUNY Korea, Eunhee Kim2e Consulting Corp.
Media Attached
17:30 - 18:00
17:30
30m
Break
Tuesday Coffee Break 2
Workshops and Co-located Events
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:00 - 18:45
Contributed TalksCoqPL at CoqPL
18:00
15m
Talk
Verification of Algorithm and Code Generation for Signal Transforms
CoqPL
Patrick BrinichDrexel University, Jeremy JohnsonDrexel University, USA
File Attached
18:15
15m
Talk
An experience report on writing usable DSLs in Coq
CoqPL
Clément Pit-ClaudelMassachusetts Institute of Technology, USA, Thomas BourgeatMIT CSAIL
File Attached
18:30
15m
Break
Break
CoqPL
18:00 - 19:30
Foundations and Programming Concepts at WorkPADL at PADL
Chair(s): Mario AlvianoUniversity of Calabria
18:00
30m
Research paper
Synchronous Message-Passing with Priority
PADL
Cheng-En ChuangUniversity at Buffalo, Grant IraciUniversity at Buffalo, Lukasz ZiarekSUNY Buffalo, USA
18:30
30m
Research paper
Putting gradual types to work
PADL
Bhargav ShivkumarState University of New York - University at Buffalo, Enrique NaudonBloomberg, Lukasz ZiarekSUNY Buffalo, USA
19:00
30m
Short-paper
Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract)
PADL
Reed OeiUniversity of Illinois at Urbana-Champaign, Michael CoblenzUniversity of Maryland at College Park, Jonathan AldrichCarnegie Mellon University
File Attached
18:00 - 19:00
Session 5PEPM at PEPM
Chair(s): Torben MogensenDIKU, University of Copenhagen

Live stream: https://www.youtube.com/watch?v=VJZcAtvGOyE

18:00
30m
Research paper
A Type-Safe Structure Editor Calculus
PEPM
Christian GodiksenDepartment of Computer Science, Aalborg University, Thomas HerrmannDepartment of Computer Science, Aalborg University, Hans HüttelDepartment of Computer Science, Aalborg University, Mikkel Korup LauridsenDepartment of Computer Science, Aalborg University, Iman OwliaieDepartment of Computer Science, Aalborg University
Media Attached
18:30
30m
Research paper
Strictly Capturing Non-Strict Closures
PEPM
Zachary SullivanUniversity of Oregon, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA
Media Attached
18:00 - 19:30
18:00
90m
Talk
SRC Finalists Presentations
Student Research Competition
18:00 - 18:30
Case StudiesVMCAI at VMCAI
Chair(s): Roderick BloemInstitute of Software Technology, Graz University of Technology
18:00
15m
Talk
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Michelle Aluf-MedinaBar Ilan University, Till KortenTU Dresden, Avraham RavivBar Ilan University, Dan Nicolau Jr.Molecular Sense, Hillel KuglerBar Ilan University
Media Attached
18:15
15m
Talk
Netter: Probabilistic, Stateful Network Models
VMCAI
Han ZhangCarnegie Mellon University, Chi Zhang, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Yuvraj AgarwalCarnegie Mellon University, Matt FredriksonCarnegie Mellon University, Limin JiaCarnegie Mellon University
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
18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. SummersUniversity of British Columbia
18:30
15m
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin BrombergerMPI-INF, Alberto FioriMax Planck Institute for Informatics, Christoph WeidenbachMPI-INF
Media Attached
18:45
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen HoenickeUniversity of Freiburg, Tanja SchindlerUniversity of Freiburg
Media Attached
19:00
15m
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias PaxianUniversity of Freiburg, Pascal RaiolaUniversity of Freiburg, Bernd BeckerAlbert-Ludwigs-University Freiburg
Media Attached
19:15
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc LeUniversity College London, UK
Media Attached
18:45 - 19:30
Session with the Coq Development TeamCoqPL at CoqPL
18:45
45m
Demonstration
Session with the Coq Development Team
CoqPL
P: Matthieu SozeauInria, P: Enrico TassiINRIA
19:30 - 20:00
19:30
30m
Break
Welcome to Copenhagen!
Workshops and Co-located Events
19:30 - 20:30
Keynote 3PEPM at PEPM
Chair(s): Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK

Live stream: https://www.youtube.com/watch?v=MMq4J8eti1g

19:30
60m
Keynote
Hardware DSLs
PEPM
Pat HanrahanStanford University, USA

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

04:30 - 05:30
04:30
60m
Social Event
Panel Discussion 3: Work/Life Balance
POPL Meetups
Andreea CosteaSchool of Computing, National University Of Singapore, Atsushi IgarashiKyoto University, Japan, KC SivaramakrishnanIIT Madras, Soham ChakrabortyIIT Delhi, India
07:00 - 08:00
07:00
60m
Break
Wednesday Coffee Break
POPL Meetups
15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Wednesday Breakfast Tables
POPL
15:45 - 16:00
WelcomePOPL at POPL
15:45
15m
Day opening
Welcome
POPL
16:00 - 17:00
Compilers & OptimizationPOPL at POPL-A
16:00
10m
Talk
Fully Abstract from Static to Gradual
POPL
Koen JacobsKU Leuven, Amin TimanyAarhus University, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
16:10
10m
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen RouvoetDelft University of Technology, Robbert KrebbersRadboud University Nijmegen, Eelco VisserDelft University of Technology
Link to publication DOI Pre-print
16:20
10m
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha HietalaUniversity of Maryland, Robert RandUniversity of Chicago, Shih-Han HungUniversity of Maryland, USA, Xiaodi WuUniversity of Maryland, USA, Michael HicksUniversity of Maryland at College Park
Link to publication DOI
16:30
10m
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël CourantINRIA, Xavier LeroyCollège de France
Link to publication DOI
16:40
10m
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes, IRISA, Olivier FlückigerNortheastern University, David PichardieUniv Rennes, ENS Rennes, IRISA, Jan VitekNortheastern University / Czech Technical University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL
16:00 - 17:00
SemanticsPOPL at POPL-B
16:00
10m
Talk
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Chao-Hong ChenIndiana University, Amr SabryIndiana University
Link to publication DOI
16:10
10m
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo AngiuliCarnegie Mellon University, Evan CavalloCarnegie Mellon University, Anders MörtbergDepartment of Mathematics, Stockholm University, Max ZeunerStockholm University
Link to publication DOI
16:20
10m
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
Ryan DoengesCornell University, Mina Tahmasbi ArashlooCornell University, Santiago BautistaUniv Rennes, ENS Rennes, Inria, IRISA, Alexander ChangCornell University, Newton NiCornell University, Samwise ParkinsonCornell University, Rudy PetersonCornell University, Alaia Solko-BreslinCornell University, Amanda XuCornell University, Nate FosterCornell University
Link to publication DOI Pre-print
16:30
10m
Talk
The (In)Efficiency of Interaction
POPL
Beniamino AccattoliInria & Ecole Polytechnique, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Gabriele VanoniUniversity of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40
10m
Talk
Functorial Semantics for Partial Theories
POPL
Chad NesterTallinn University of Technology, Ivan Di LibertiCzech Academy of Sciences, Fosco LoregianTallinn University of Technology, Pawel SobocinskiTallinn University of Technology
Link to publication DOI
16:50
10m
Break
Break
POPL
18:00 - 18:30
SocialPOPL at Break
18:30 - 19:30
Program AnalysisPOPL at POPL-A
18:30
10m
Talk
Verifying Correct Usage of Context-Free API Protocols
POPL
Kostas FerlesUT Austin, Jon StephensUniversity of Texas at Austin, Isil DilligUniversity of Texas at Austin
Link to publication DOI
18:40
10m
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir PavlinovicGoogle, USA, Yusen SuNew York University, University of Waterloo, Thomas WiesNew York University, USA
Link to publication DOI
18:50
10m
Talk
An Approach to Generate Correctly Rounded Math Libraries for New Floating Point Variants
POPL
Jay P. LimRutgers University, USA, Mridul AanjaneyaRutgers University, John GustafsonNational University of Singapore, Santosh NagarakatteRutgers University, USA
Link to publication DOI
19:00
10m
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian RosemannSaarland University, Saarland Informatics Campus, Simon MollNEC Deutschland, Sebastian HackSaarland University, Germany
Link to publication DOI
19:10
10m
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaETH Zurich
Link to publication DOI
19:20
10m
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban ReynaudENS Lyon, Gabriel SchererINRIA Saclay, Jeremy YallopUniversity of Cambridge
Link to publication DOI Pre-print
18:30 - 19:30
Types and Proof AssistancePOPL at POPL-B
18:30
10m
Talk
Asynchronous Effects
POPL
Danel AhmanUniversity of Ljubljana, Matija PretnarUniversity of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas SilverUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet RajaniMPI-SP, Marco GaboardiBoston University, Deepak GargMax Planck Institute for Software Systems, Jan HoffmannCarnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam ChoudhuryUniversity of Pennsylvania, Harley D. Eades IIIAugusta University, Richard A. EisenbergTweag I/O, Stephanie WeirichUniversity of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron MoyNortheastern University, Phúc C. NguyễnGoogle, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland, USA
Link to publication DOI Pre-print
19:20
10m
Talk
The Taming of the Rew: A Type Theory with Computational Assumptions
POPL
Jesper CockxTU Delft, Nicolas TabareauInria, Théo WinterhalterInria — LS2N
Link to publication DOI Pre-print
19:30 - 20:00
SocialPOPL at Break
19:30
30m
Social Event
Happy Hour
POPL
19:30 - 20:00
Sponsor ReceptionPOPL at POPL
19:30
30m
Industry talk
Sponsor Reception
POPL
Media Attached
20:00 - 21:00
SocialPOPL at Break

After Hours

20:00
60m
Social Event
Trivia Night
POPL
20:00 - 20:30
20:00
30m
Meeting
SIGPLAN CARES
POPL
P: Stephanie WeirichUniversity of Pennsylvania, P: Alexandra SilvaUniversity College London, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA

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

02:00 - 03:00
SocialPOPL at Break

After Hours

02:00
60m
Social Event
POPL Cocktail Hour
POPL
04:00 - 04:30
04:00
30m
Meeting
SIGPLAN CARES
POPL
P: Stephanie WeirichUniversity of Pennsylvania, P: Hongseok YangKAIST, P: Shriram KrishnamurthiBrown University, United States, P: David WalkerPrinceton University, USA
04:30 - 05:30
04:30
60m
Social Event
Panel Discussion 4: Finding Friends and Collaborators in Academia
POPL Meetups
Aseem RastogiMicrosoft Research, Atsushi IgarashiKyoto University, Japan, Christine RizkallahUNSW Sydney, Jeehoon KangKAIST, Youyou CongTokyo Institute of Technology
07:00 - 08:00
07:00
60m
Break
Thursday Coffee Break
POPL Meetups
15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Topic Oriented Discussions
POPL
15:45 - 15:55
Most Influential POPL PaperPOPL at POPL
15:45
10m
Awards
Most Influential POPL Paper
POPL
Media Attached
15:55 - 16:00
Student Research Competition ResultsStudent Research Competition at POPL
15:55
5m
Awards
Student Research Competition Results
Student Research Competition
16:00 - 17:00
SecurityPOPL at POPL-A
16:00
10m
Talk
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Thomas Van StrydonckKULeuven, Amin TimanyAarhus University, Alix TrieuAarhus University, Sander HuyghebaertVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:10
10m
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede GregersenAarhus University, Johan BayAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:20
10m
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew HirschMax Planck Institute for Software Systems, Ethan CecchettiCornell University
Link to publication DOI
16:30
10m
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver GutsfeldWestfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-OlmUniversity of Münster, Christoph OhremWestfälische Wilhelms-Universität Münster (WWU), Germany
Link to publication DOI
16:40
10m
Talk
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Marco VassenaCISPA Helmholtz Center for Information Security, Craig DisselkoenUniversity of California at San Diego, USA, Klaus v. GleissenthallVrije Universiteit Amsterdam, Netherlands, Sunjay CauligiUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, Dean TullsenUniversity of California at San Diego, USA, Deian StefanUniversity of California at San Diego, USA
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL
16:00 - 17:00
Concurrency (Shared Memory)POPL at POPL-B
16:00
10m
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy MargalitTel Aviv University, Israel, Ori LahavTel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin AroraCMU, Sam WestrickCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. MullerIllinois Institute of Technology, Jan HoffmannCarnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang MathurUniversity of Illinois at Urbana-Champaign, Andreas PavlogiannisAarhus University, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem KhyzhaTel Aviv University, Ori LahavTel Aviv University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL
17:00 - 18:00
Invited TalkPOPL at POPL
17:00
60m
Keynote
Dynamical Systems and Program AnalysisInvited Talk
POPL
James WorrellUniversity of Oxford
File Attached
18:00 - 18:30
SocialPOPL at Break
18:30 - 19:30
ComplexityPOPL at POPL-A
18:30
10m
Talk
Learning the Boundary of Inductive Invariants
POPL
Yotam M. Y. FeldmanTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv University, James R. WilcoxUniversity of Washington
Link to publication DOI
18:40
10m
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas PavlogiannisAarhus University, Anders Alnor MathiasenAarhus University
Link to publication DOI
18:50
10m
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal BaumannMax Planck Institute for Software Systems (MPI-SWS), Rupak MajumdarMPI-SWS, Ramanathan S. ThinniyamMax Planck Institute for Software Systems (MPI-SWS), Georg ZetzscheMax Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00
10m
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull AlmagorTechnion, Toghrul KarimovMax Planck Institute for Software Systems, Edon KelmendiUniversity of Oxford, Joël OuaknineMax Planck Institute for Software Systems and University of Oxford, James WorrellUniversity of Oxford
Link to publication DOI
19:10
10m
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Ahmed BouajjaniIRIF, Université Paris Diderot, K Narayan KumarChennai Mathematical Institute, Prakash SaivasanThe Institute of Mathematical Sciences, India
Link to publication DOI
19:20
10m
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo LiGeorgia Institute of Technology, USA, Qirun ZhangGeorgia Institute of Technology, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI
18:30 - 19:30
Types and Functional LanguagesPOPL at POPL-B
18:30
10m
Talk
Diamonds Are Not Forever: Liveness in Reactive Programming with Guarded Recursion
POPL
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
Link to publication DOI
18:40
10m
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco PatrignaniStanford University, USA / CISPA, Germany, Eric Mark MartinStanford, Dominique DevrieseVrije Universiteit Brussel
Link to publication DOI
18:50
10m
Talk
Automatic Differentiation in PCF
POPL
Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris
Link to publication DOI Pre-print
19:00
10m
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Claudia FaggianUniversité de Paris & CNRS, Simona Ronchi Della RoccaUniversity of Torino
Link to publication DOI
19:10
10m
Talk
Intensional Datatype Refinement
POPL
Eddie JonesUniversity of Bristol, Steven RamsayUniversity of Bristol
Link to publication DOI
19:20
10m
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados SchwerterUniversity of British Columbia, Alison M. ClarkUniversity of British Columbia, Khurram A. JaferyUniversity of British Columbia, Ronald GarciaUniversity of British Columbia
Link to publication DOI
19:30 - 20:30
Business MeetingPOPL at POPL
19:30
60m
Meeting
Business Meeting & Townhall
POPL
20:30 - 21:30
20:30
60m
Meeting
Iris meetup
POPL Meetups
21:00 - 22:00
21:00
60m
Social Event
Games Programming Languages BoF Session
POPL Meetups

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

07:00 - 08:00
07:00
60m
Break
Friday Coffee Break
POPL Meetups
15:15 - 15:45
SocialPOPL at Break
15:15
30m
Social Event
Friday Breakfast Tables
POPL
15:45 - 16:45
Probabilistic ProgrammingPOPL at POPL-A
15:45
10m
Talk
λS: Computable Semantics for Differentiable Programming with Higher-Order Functions and Datatypes
POPL
Benjamin ShermanMassachusetts Institute of Technology, USA, Jesse MichelMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology
Link to publication DOI
15:55
10m
Talk
Deciding Accuracy of Differential Privacy Schemes
POPL
Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Rohit ChadhaUniversity of Missouri, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, A. Prasad SistlaUniversity of Illinois at Chicago, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI
16:05
10m
Talk
Probabilistic Programming Semantics for Name Generation
POPL
Marcin SabokMcGill University, Sam StatonUniversity of Oxford, Dario SteinUniversity of Oxford, Michael WolmanMcGill University
Link to publication DOI Pre-print
16:15
10m
Talk
Simplifying Multiple-Statement Reductions with the Polyhedral Model
POPL
Cambridge YangMIT CSAIL, Eric AtkinsonMIT CSAIL, Michael CarbinMassachusetts Institute of Technology
Link to publication DOI
16:25
10m
Talk
A Pre-Expectation Calculus for Probabilistic SensitivityDistinguished Paper
POPL
Alejandro AguirreIMDEA Software Institute and T.U. of Madrid (UPM), Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Justin HsuUniversity of Wisconsin-Madison, USA, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaETH Zurich
Link to publication DOI
16:35
10m
Talk
Paradoxes of probabilistic programming
POPL
Jules JacobsRadboud University Nijmegen
Link to publication DOI Pre-print
15:45 - 16:45
Concurrency (Message Passing)POPL at POPL-B
15:45
10m
Talk
On Algebraic Abstractions for Concurrent Separation Logics
POPL
František FarkaIMDEA Software Institute, Spain, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoNomadic Labs, Ignacio FábregasUniversidad Complutense de Madrid
Link to publication DOI
15:55
10m
Talk
Transfinite Step-Indexing for Termination
POPL
Simon SpiesMPI-SWS and University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Derek DreyerMPI-SWS
Link to publication DOI
16:05
10m
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia GhilezanUniversity of Novi Sad, Mathematical Institute SASA, Jovanka PantovićUniversity of Novi Sad, Ivan ProkićUniversity of Novi Sad, Alceste ScalasTechnical University of Denmark, Nobuko YoshidaImperial College London
Link to publication DOI Media Attached
16:15
10m
Talk
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
16:25
10m
Talk
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Léon GondelmanAarhus University, Simon Oddershede GregersenAarhus University, Abel NietoAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI
16:35
10m
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis KokologiannakisMPI-SWS, Germany, Ilya KaysinNational Research University Higher School of Economics, JetBrains Research, Azalea RaadImperial College London, Viktor VafeiadisMPI-SWS
Link to publication DOI
16:45 - 17:00
BreakPOPL at Break
16:45
15m
Break
Break
POPL
18:00 - 18:30
SocialPOPL at Break
18:30 - 19:00
SynthesisPOPL at POPL-A
18:30
10m
Talk
Generating Collection Transformations from Proofs
POPL
Michael BenediktUniversity of Oxford, UK, Pierre PradicOxford University
Link to publication DOI
18:40
10m
Talk
Semantics-Guided Synthesis
POPL
Jinwoo KimUniversity of Wisconsin-Madison, Qinheping HuUniversity of Wisconsin-Madison, USA, Loris D'AntoniUniversity of Wisconsin-Madison, USA, Thomas RepsUniversity of Wisconsin--Madison
Link to publication DOI
18:50
10m
Talk
Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis
POPL
Woosuk LeeHanyang University, South Korea
Link to publication DOI
18:30 - 19:00
Logic and Decision ProceduresPOPL at POPL-B
18:30
10m
Talk
Cyclic Proofs, System T, and the Power of Contraction
POPL
Denis KuperbergLIP, ENS de Lyon, Laureline PinaultLIP, ENS de Lyon, Damien PousCNRS
Link to publication DOI
18:40
10m
Talk
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Max WillseyUniversity of Washington, USA, Chandrakana NandiUniversity of Washington, USA, Yisu Remy WangUniversity of Washington, Oliver FlattUniversity of Utah, Zachary TatlockUniversity of Washington, Seattle, Pavel PanchekhaUniversity of Utah
Link to publication DOI Pre-print
18:50
10m
Talk
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
POPL
David ZhaoThe University of Sydney, Pavle SuboticMicrosoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard ScholzUniversity of Sydney, Australia
Link to publication DOI
19:00 - 20:00
Robin Milner AwardPOPL at POPL
19:00
60m
Awards
Robin Milner Award Talk: "Structural Language Models of Code"
POPL
R: Eran YahavTechnion, A: Emery D. BergerUniversity of Massachusetts Amherst
Media Attached
20:00 - 20:30
SocialPOPL at Break

After Hours

20:00
30m
Social Event
Farewell Reception
POPL
21:00 - 22:00
21:00
60m
Meeting
Iris meetup #2
POPL Meetups