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

Dates
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

Displayed 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 - 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
16:00 - 16:50
Invited talk: Vikash K. MansinghkaLAFI at LAFI
Chair(s): Jean-Baptiste Tristan Boston College
16:00 - 17:30
Secure compilers & cryptographyPriSC at PriSC
Chair(s): Fraser Brown Stanford University, USA, Aastha Mehta MPI-SWS, Germany and University of British Columbia, Canada
16:00
18m
Talk
High-level high-speed high-assurance crypto
PriSC
Jonathan Cogan Stanford, Fraser Brown Stanford University, USA, Alex Ozdemir Stanford, Riad S. Wahby Stanford University, USA
Media Attached
16:18
18m
Talk
Cross-Architecture Testing for Compiler-Introduced Security Bugs
PriSC
Jianhao Xu Nanjing University, Kangjie Lu University of Minnesota, Bing Mao Nanjing University
Media Attached File Attached
16:36
18m
Talk
High-Assurance Cryptography in the Spectre Era
PriSC
Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Sunjay Cauligi University of California at San Diego, USA, Benjamin Gregoire INRIA, Adrien Koutsos INRIA Paris, Kevin Liao Max Planck Institute for Security and Privacy, Tiago Oliveira University of Porto (FCUP) and INESC TEC, Swarn Priya Purdue University, Tamara Rezk Inria, France, Peter Schwabe Max Planck Institute for Security and Privacy
Media Attached
16:54
18m
Talk
Compilation as Multi-Language Semantics
PriSC
William J. Bowman University of British Columbia
Pre-print Media Attached
17:12
18m
Talk
Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs
PriSC
Coşku Acay Cornell University, Rolph Recto , Joshua Gancher Cornell University, Andrew C. Myers Cornell University, Elaine Shi Cornell University
Media Attached
16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
Model Checking Hyperproperties
VMCAI
I: Bernd Finkbeiner CISPA Helmholtz Center for Information Security
Media Attached
16:50 - 17:30
Session 1LAFI at LAFI
Chair(s): Jean-Baptiste Tristan Boston College
16:50
13m
Talk
Binary Tree Hamiltonian Monte Carlo
LAFI
Carol Mak University of Oxford, Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford
File Attached
17:03
13m
Talk
An algebraic theory of conditioning
LAFI
Dario Stein University of Oxford, Sam Staton University 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 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
17:00 - 17:30
HyperpropertiesVMCAI at VMCAI
Chair(s): Grigory Fedyukovich Florida State University
17:00
15m
Talk
Compositional Model Checking for Multi-Properties
VMCAI
Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of Engineering
Media Attached
17:15
15m
Talk
Decomposing Data Structure Commutativity Proofs with mn-Differencing
VMCAI
Eric Koskinen Stevens Institute of Technology, Kshitij Bansal Google
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 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:00 - 19:30
Session 2LAFI at LAFI
Chair(s): Dougal Maclaurin Google Research
18:00
12m
Talk
Enzyme: High-Performance Automatic Differentiation of LLVM
LAFI
William S. Moses Massachusetts Institute of Technology, Valentin Churavy MIT CSAIL
18:12
12m
Talk
Parametric Inversion of Non-Invertible Programs
LAFI
Zenna Tavares Massachusetts Institute of Technology, Javier Burroni University of Massachusetts Amherst, Edgar Minasyan Princeton University, David Morejon Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology
File Attached
18:25
12m
Talk
Bayesian Neural Ordinary Differential Equations
LAFI
Raj Dandekar MIT, Vaibhav Dixit Julia Computing, Mohamed Tarek UNSW Canberra, Australia, Aslan Garcia Valadez National Autonomous University of Mexico, Chris Rackauckas MIT
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. Lew Massachusetts Institute of Technology, USA, Ben Sherman , Marco Cusumano-Towner MIT-CSAIL, Michael Carbin Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
Media Attached
18:51
12m
Talk
Decomposing reverse-mode automatic differentiation
LAFI
Roy Frostig Google Research, Matthew Johnson Google Brain, Dougal Maclaurin Google Research, Adam Paszke Google Research, Alexey Radul Google Research
File Attached
19:04
12m
Talk
Genify.jl: Transforming Julia into Gen to enable programmable inference
LAFI
Tan Zhi-Xuan Massachusetts Institute of Technology, McCoy R. Becker Charles River Analytics, Vikash K. Mansinghka MIT
Media Attached File Attached
19:17
12m
Talk
Probabilistic Inference Using Generators: the Statues Algorithm
LAFI
Pierre Denis independent scholar
Link to publication DOI Pre-print Media Attached File Attached
18:00 - 19:00
Invited talkPriSC at PriSC
Chair(s): Deian Stefan University of California at San Diego, USA
18:00
60m
Keynote
Frontiers in Secure Compilation – an Industrial Perspective (invited talk)
PriSC
Hugo Vincent Arm 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 Grumberg Technion – Israel Institute of Technology
18:00
15m
Talk
Proving the existence of fair paths in infinite state systems
VMCAI
Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler
Media Attached
18:15
15m
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar Namjoshi Nokia Bell Labs, Anton Xue University of Pennsylvania
Media Attached
18:30 - 19:30
Concurrent and Distributed SystemsVMCAI at VMCAI
Chair(s): Dana Drachsler Cohen Technion
18:30
15m
Talk
Concurrent Correctness in Vector Space
VMCAI
Christina Peterson University of Central Florida, Victor Cook University of Central Florida, Damian Dechev University of Central Florida
Media Attached
18:45
15m
Talk
Verification of Concurrent Programs Using Petri Net Unfoldings
VMCAI
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Mehdi Naouar University of Freiburg, Andreas Podelski University of Freiburg, Germany, Claus Schätzle University of Freiburg
Media Attached
19:00
15m
Talk
Eliminating Message Counters in Synchronous Threshold Automata
VMCAI
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Informal Systems Inc, Josef Widder Informal Systems, Florian Zuleger Vienna University of Technology
Media Attached
19:15
15m
Talk
A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
VMCAI
Nathalie Bertrand INRIA Rennes, Marijana Lazic Technical University of Munich, Josef Widder Informal Systems
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
19:00 - 20:30
Formal analysis & proof techniquesPriSC at PriSC
Chair(s): Marco Patrignani Stanford University, USA / CISPA, Germany, Jonathan Protzenko Microsoft 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 Gourjon Hamburg University of Technology and NXP Semiconductors Germany GmbH
Media Attached
19:36
18m
Talk
Secure Optimization Through Opaque Observations
PriSC
Son Tuan Vu Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert Cohen Google, Karine Heydemann Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Arnaud de Grandmaison ARM, Christophe Guillon STMicroelectronics
Pre-print Media Attached File Attached
19:54
18m
Talk
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università 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 Georges Aarhus University, Armaël Guéneau Aarhus University, Alix Trieu Aarhus University, Lars Birkedal Aarhus 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 Stefan University of California at San Diego, USA
21:00
15m
Talk
A Categorical Approach to Secure Compilation (and others things) (short talk)
PriSC
Stelios Tsampas , Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel, Frank Piessens KU Leuven
21:15
15m
Talk
Contract-aware Secure Compilation (short talk)
PriSC
Marco Guarnieri ETH Zurich, Switzerland, Marco Patrignani Stanford University, USA / CISPA, Germany
Pre-print

Mon 18 Jan

Displayed 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 Hur Seoul National University, South Korea, Christine Rizkallah UNSW Sydney, Hongseok Yang KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, James Noble Victoria 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 Mogensen DIKU, 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 Asai Ochanomizu University, Youyou Cong Tokyo Institute of Technology, Chiaki Ishio Ochanomizu University
Media Attached File Attached
10:30
30m
Research paper
A Text-based Syntax Completion Method Using LR Parsing
PEPM
Isao Sasano Shibaura Institute of Technology, Kwanghoon Choi Chonnam National University
Media Attached
11:30 - 12:30
Session 2PEPM at PEPM
Chair(s): Youyou Cong Tokyo 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 Tanaka National 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 Ueno The Univeristy of Tokyo, John Toman Certora, inc., Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan
Media Attached
13:30 - 14:30
Session 3PEPM at PEPM
Chair(s): Robert Atkey University 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 Lu ISTD, Singapore University of Technology and Design
Media Attached File Attached
14:00
30m
Research paper
Efficient Fair Conjunction for Structurally-Recursive Relations
PEPM
Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research
Media Attached File Attached
14:30 - 15:30
Keynote 1PADL at PADL
Chair(s): Dominic Orchard University of Kent, UK
14:30
60m
Keynote
Semantics-based Synthesis in miniKanren
PADL
William E. Byrd University of Alabama at Birmingham, USA
14:30 - 15:15
Session 0PLMW at PLMW
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:30
45m
Talk
Think Abstractly, Work Concretely
PLMW
Ichiro Hasuo National Institute of Informatics, Japan
Media Attached
15:00 - 16:00
Keynote 1PEPM at PEPM
Chair(s): Sam Lindley Heriot-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 Komendantskaya Heriot-Watt University, UK
16:00
30m
Research paper
A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States
PADL
Fabio Tardivo New Mexico State University, Loc Pham New Mexico State University, Tran Cao Son New Mexico State University, Enrico Pontelli New Mexico State University
16:30
30m
Research paper
Data validation meets Answer Set Programming
PADL
Mario Alviano University of Calabria, Carmine Dodaro Department of Mathematics and Computer Science, University of Calabria, Arnel Zamayla University of Calabria, Italy
17:00
30m
Research paper
Lightweight Declarative Server-Side Web Programming
PADL
Michael Hanus Kiel University
16:00 - 17:30
Session 1PLMW at PLMW
Chair(s): Azalea Raad Imperial 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. Donaldson Imperial College London and Google
16:00 - 17:30
16:00
90m
Tutorial
[T1] The Current State of Automatic Differentiation
TutorialFest
Barak A. Pearlmutter Maynooth University
16:00 - 17:30
16:00
90m
Tutorial
[T2] Liquid Haskell: Refinement Type Checker for Haskell
TutorialFest
Niki Vazou IMDEA Software Institute, Andres Löh Well-Typed LLP
16:00 - 17:30
16:00
90m
Tutorial
[T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice
TutorialFest
Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University
Pre-print Media Attached File Attached
16:00 - 17:00
Invited talkVMCAI at VMCAI
Chair(s): Yakir Vizel Technion—Israel Institute of Technology
16:00
60m
Keynote
Algebra-based Synthesis of Loops and their Invariants
VMCAI
I: Laura Kovacs Vienna University of Technology (TU Wien), Andreas Humenberger Vienna University of Technology
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
17:00 - 17:30
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
17:00
15m
Talk
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LIST
Media Attached
17:15
15m
Talk
Twinning automata and regular expressions for string static analysis
VMCAI
Luca Negrini Ca’ Foscari University of Venice, Julia S.r.l., Vincenzo Arceri Ca’ Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università 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 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:00 - 19:30
Foundations and Programming ConceptsPADL at PADL
Chair(s): Dominic Orchard University of Kent, UK
18:00
30m
Research paper
A Family of Unification-oblivious Program Transformations and Their Applications
PADL
Paul Tarau University of North Texas
18:30
30m
Research paper
On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages
PADL
David Young University of Kansas, USA, Mark Grebe University of Central Missouri, USA, Andy Gill University of Kansas, USA
18:00 - 19:30
18:00
90m
Tutorial
[T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic
TutorialFest
Tej Chajed Massachusetts Institute of Technology, USA, Ralf Jung MPI-SWS, Joseph Tassarotti Boston College
Link to publication
18:00 - 18:30
Model CheckingVMCAI at VMCAI
Chair(s): James R. Wilcox University of Washington
18:00
15m
Talk
Unbounded Procedure Summaries from Bounded Environments
VMCAI
Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University
Media Attached
18:15
15m
Talk
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
VMCAI
Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton University
Media Attached
18:30 - 19:15
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws Albarghouthi University of Wisconsin-Madison, USA
18:30
15m
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45
15m
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
19:00
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh Joshi IIT Hyderabad, Gautam Muduganti IIT Hyderabad
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
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 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, Antonio 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
20:00 - 21:00
Monday PanelPLMW at PLMW
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
20:00
60m
Live Q&A
Panel: Doing Research in PL
PLMW
Greg Morrisett Cornell Tech, Susan Eisenbach Imperial College London, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, Jeehoon Kang KAIST, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities

Tue 19 Jan

Displayed 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 Yang KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, James Noble Victoria University of Wellington, Soham Chakraborty IIT Delhi, India, Youyou Cong Tokyo 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é Morales IMDEA Software Institute
14:30
60m
Keynote
SMT-based Constraint Answer Set Solver EZSMT
PADL
Yuliya Lierler University of Nebraska
14:30 - 15:30
Tuesday PanelPLMW at PLMW
Chair(s): Stephanie Balzer Carnegie Mellon University, USA
14:30
60m
Live Q&A
Panel: Navigating PhD studies
PLMW
Hila Peleg University of California at San Diego, Nick Giannarakis University of Wisconsin-Madison, Anne-Kathrin Schmuck MPI-SWS, Sacha-Élie Ayoun Imperial College London, Farzaneh Derakhshan Carnegie Mellon University, Soham Chakraborty IIT Delhi
15:00 - 16:00
Keynote 2PEPM at PEPM
Chair(s): Torben Mogensen DIKU, 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 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:00 - 17:30
Contributed TalksCoqPL at CoqPL
16:00
15m
Talk
A Limited Case for Reification by Type Inference
CoqPL
Jason Gross MIT CSAIL
Media Attached File Attached
16:15
15m
Talk
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
CoqPL
Xuanrui Qi Nagoya University, Jacques Garrigue Nagoya University
File Attached
16:30
15m
Talk
Record Updates in Coq
CoqPL
Tej Chajed Massachusetts 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-Kirilyuk Harvard University, Andrew Appel Princeton, Lennart Beringer Princeton University
File Attached
17:15
15m
Talk
Automated Synthesis of Verified Firewalls
CoqPL
Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology
File Attached
16:00 - 17:30
Declarative Approaches to Testing and DebuggingPADL at PADL
Chair(s): Paul Tarau University of North Texas
16:00
30m
Research paper
ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs
PADL
Sumit Padhiyar Indian Institue Of Technology, Madras, KC Sivaramakrishnan IIT Madras
Link to publication
16:30
30m
Research paper
Causal-Consistent Reversible Debugging: Improving CauDEr
PADL
Juan José González-Abril MiST, VRAIN, Universitat Politecnica de Valencia, German Vidal Universitat Politecnica de Valencia
17:00
30m
Research paper
Declarative Debugging of XML Queries
PADL
Jesus M. Almendros-Jimenez Universidad de Almeria, Antonio Becerra-Teron University of Almeria
16:00 - 17:30
Session 3PLMW at PLMW
Chair(s): Azalea Raad Imperial College London
16:00
45m
Talk
Connecting Information Flow Types to Runtime Monitors via Gradual Typing
PLMW
Limin Jia Carnegie 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 Steffen TU Dortmund, Alnis Murtovi TU Dortmund, David Schmidt Kansas State University
Media Attached
16:30 - 17:30
Session 4PEPM at PEPM
Chair(s): Jeremy Yallop University of Cambridge

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

16:30
30m
Short-paper
Staged Effects and Handlers for Modular Languages with Abstraction
PEPM
Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology, Tom Schrijvers KU Leuven
Media Attached File Attached
17:00
30m
Short-paper
Automatic Differentiation via Effects and Handlers: An Implementation in Frank
PEPM
Jesse Sigal University of Edinburgh
Media Attached File 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
17:00 - 17:30
ApplicationsVMCAI at VMCAI
Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security
17:00
15m
Talk
A Synchronous Effects Logic for Temporal Verification of Pure Esterel
VMCAI
Yahui Song National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
17:15
15m
Talk
A Design of GPU-Based Quantitative Model Checking
VMCAI
YoungMin Kwon SUNY Korea, Eunhee Kim 2e 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 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:00 - 18:45
Contributed TalksCoqPL at CoqPL
18:00
15m
Talk
Verification of Algorithm and Code Generation for Signal Transforms
CoqPL
Patrick Brinich Drexel University, Jeremy Johnson Drexel University, USA
File Attached
18:15
15m
Talk
An experience report on writing usable DSLs in Coq
CoqPL
Clément Pit-Claudel Massachusetts Institute of Technology, USA, Thomas Bourgeat MIT CSAIL
File Attached
18:30
15m
Break
Break
CoqPL

18:00 - 19:30
Foundations and Programming Concepts at WorkPADL at PADL
Chair(s): Mario Alviano University of Calabria
18:00
30m
Research paper
Synchronous Message-Passing with Priority
PADL
Cheng-En Chuang University at Buffalo, Grant Iraci University at Buffalo, Lukasz Ziarek SUNY Buffalo, USA
18:30
30m
Research paper
Putting gradual types to work
PADL
Bhargav Shivkumar State University of New York - University at Buffalo, Enrique Naudon Bloomberg, Lukasz Ziarek SUNY Buffalo, USA
19:00
30m
Short-paper
Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract)
PADL
Reed Oei University of Illinois at Urbana-Champaign, Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University
File Attached
18:00 - 19:00
Session 5PEPM at PEPM
Chair(s): Torben Mogensen DIKU, 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 Godiksen Department of Computer Science, Aalborg University, Thomas Herrmann Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mikkel Korup Lauridsen Department of Computer Science, Aalborg University, Iman Owliaie Department of Computer Science, Aalborg University
Media Attached
18:30
30m
Research paper
Strictly Capturing Non-Strict Closures
PEPM
Zachary Sullivan University of Oregon, Paul Downen University of Oregon, USA, Zena M. Ariola University 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 Bloem Institute of Software Technology, Graz University of Technology
18:00
15m
Talk
Formal Semantics and Verification of Network Based Biocomputation Circuits
VMCAI
Michelle Aluf-Medina Bar Ilan University, Till Korten TU Dresden, Avraham Raviv Bar Ilan University, Dan Nicolau Jr. Molecular Sense, Hillel Kugler Bar Ilan University
Media Attached
18:15
15m
Talk
Netter: Probabilistic, Stateful Network Models
VMCAI
Han Zhang Carnegie Mellon University, Chi Zhang , Arthur Azevedo de Amorim Carnegie Mellon University, USA, Yuvraj Agarwal Carnegie Mellon University, Matt Fredrikson Carnegie Mellon University, Limin Jia Carnegie 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ţcu MPI-SP, Andrei Popescu University of Sheffield, Lennart Beringer Princeton University
Media Attached File Attached
18:30 - 19:30
Decision ProceduresVMCAI at VMCAI
Chair(s): Alexander J. Summers University of British Columbia
18:30
15m
Talk
Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
VMCAI
Martin Bromberger MPI-INF, Alberto Fiori Max Planck Institute for Informatics, Christoph Weidenbach MPI-INF
Media Attached
18:45
15m
Talk
Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
VMCAI
Jochen Hoenicke University of Freiburg, Tanja Schindler University of Freiburg
Media Attached
19:00
15m
Talk
On Pre- and Inprocessing for Weighted MaxSAT
VMCAI
Tobias Paxian University of Freiburg, Pascal Raiola University of Freiburg, Bernd Becker Albert-Ludwigs-University Freiburg
Media Attached
19:15
15m
Talk
Compositional Satisfiability Solving in Separation Logic
VMCAI
Quang Loc Le University 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 Sozeau Inria, P: Enrico Tassi INRIA
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 Lindley Heriot-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 Hanrahan Stanford University, USA

Wed 20 Jan

Displayed 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 Costea School of Computing, National University Of Singapore, Atsushi Igarashi Kyoto University, Japan, KC Sivaramakrishnan IIT Madras, Soham Chakraborty IIT 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 Jacobs KU Leuven, Amin Timany Aarhus University, Dominique Devriese Vrije Universiteit Brussel
Link to publication DOI
16:10
10m
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen Rouvoet Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
Link to publication DOI Pre-print
16:20
10m
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu University of Maryland, USA, Michael Hicks University of Maryland at College Park
Link to publication DOI
16:30
10m
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël Courant INRIA, Xavier Leroy Collège de France
Link to publication DOI
16:40
10m
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes, IRISA, Olivier Flückiger Northeastern University, David Pichardie Univ Rennes, ENS Rennes, IRISA, Jan Vitek Northeastern 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 Chen Indiana University, Amr Sabry Indiana University
Link to publication DOI
16:10
10m
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm University
Link to publication DOI
16:20
10m
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University
Link to publication DOI Pre-print
16:30
10m
Talk
The (In)Efficiency of Interaction
POPL
Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40
10m
Talk
Functorial Semantics for Partial Theories
POPL
Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn 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 Ferles UT Austin, Jon Stephens University of Texas at Austin, Isil Dillig University of Texas at Austin
Link to publication DOI
18:40
10m
Talk
Data Flow Refinement Type Inference
POPL
Zvonimir Pavlinovic Google, USA, Yusen Su New York University, University of Waterloo, Thomas Wies New 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. Lim Rutgers University, USA, Mridul Aanjaneya Rutgers University, John Gustafson National University of Singapore, Santosh Nagarakatte Rutgers University, USA
Link to publication DOI
19:00
10m
Talk
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow GraphsDistinguished Paper
POPL
Julian Rosemann Saarland University, Saarland Informatics Campus, Simon Moll NEC Deutschland, Sebastian Hack Saarland University, Germany
Link to publication DOI
19:10
10m
Talk
Relatively Complete Verification of Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja ETH Zurich
Link to publication DOI
19:20
10m
Talk
A Practical Mode System for Recursive Definitions
POPL
Alban Reynaud ENS Lyon, Gabriel Scherer INRIA Saclay, Jeremy Yallop University 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 Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia
Link to publication DOI Pre-print
18:40
10m
Talk
Dijkstra Monads Forever
POPL
Lucas Silver University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Link to publication DOI
18:50
10m
Talk
A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis
POPL
Vineet Rajani MPI-SP, Marco Gaboardi Boston University, Deepak Garg Max Planck Institute for Software Systems, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
19:00
10m
Talk
A Graded Dependent Type System with a Usage-Aware Semantics
POPL
Pritam Choudhury University of Pennsylvania, Harley D. Eades III Augusta University, Richard A. Eisenberg Tweag I/O, Stephanie Weirich University of Pennsylvania
Link to publication DOI Pre-print
19:10
10m
Talk
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
POPL
Cameron Moy Northeastern University, Phúc C. Nguyễn Google, Sam Tobin-Hochstadt Indiana University, David Van Horn University 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 Cockx TU Delft, Nicolas Tabareau Inria, Théo Winterhalter Inria — 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 Weirich University of Pennsylvania, P: Alexandra Silva University College London, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA

Thu 21 Jan

Displayed 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 Weirich University of Pennsylvania, P: Hongseok Yang KAIST, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA
04:30 - 05:30
04:30
60m
Social Event
Panel Discussion 4: Finding Friends and Collaborators in Academia
POPL Meetups
Aseem Rastogi Microsoft Research, Atsushi Igarashi Kyoto University, Japan, Christine Rizkallah UNSW Sydney, Jeehoon Kang KAIST, Youyou Cong Tokyo 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 Georges Aarhus University, Armaël Guéneau Aarhus University, Thomas Van Strydonck KULeuven, Amin Timany Aarhus University, Alix Trieu Aarhus University, Sander Huyghebaert Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel, Lars Birkedal Aarhus University
Link to publication DOI Pre-print
16:10
10m
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede Gregersen Aarhus University, Johan Bay Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
Link to publication DOI Pre-print
16:20
10m
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew K. Hirsch Max Planck Institute for Software Systems, Ethan Cecchetti Cornell University
Link to publication DOI
16:30
10m
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem Westfä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 Vassena CISPA Helmholtz Center for Information Security, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, Dean Tullsen University of California at San Diego, USA, Deian Stefan University 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 Margalit Tel Aviv University, Israel, Ori Lahav Tel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin Arora CMU, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. Muller Illinois Institute of Technology, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem Khyzha Tel Aviv University, Ori Lahav Tel 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 Worrell University 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. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox University of Washington
Link to publication DOI
18:40
10m
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas Pavlogiannis Aarhus University, Anders Alnor Mathiasen Aarhus University
Link to publication DOI
18:50
10m
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal Baumann Max Planck Institute for Software Systems (MPI-SWS), Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Max Planck Institute for Software Systems (MPI-SWS), Georg Zetzsche Max Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00
10m
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull Almagor Technion, Toghrul Karimov Max Planck Institute for Software Systems, Edon Kelmendi University of Oxford, Joël Ouaknine Max Planck Institute for Software Systems and University of Oxford, James Worrell University of Oxford
Link to publication DOI
19:10
10m
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India
Link to publication DOI
19:20
10m
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo Li Georgia Institute of Technology, USA, Qirun Zhang Georgia Institute of Technology, USA, Thomas Reps University 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 Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
Link to publication DOI
18:40
10m
Talk
On the Semantic Expressiveness of Recursive Types
POPL
Marco Patrignani Stanford University, USA / CISPA, Germany, Eric Mark Martin Stanford, Dominique Devriese Vrije Universiteit Brussel
Link to publication DOI
18:50
10m
Talk
Automatic Differentiation in PCF
POPL
Damiano Mazza CNRS, Michele Pagani IRIF - Université de Paris
Link to publication DOI Pre-print
19:00
10m
Talk
Intersection Types and (Positive) Almost-Sure Termination
POPL
Ugo Dal Lago University of Bologna, Italy / Inria, France, Claudia Faggian Université de Paris & CNRS, Simona Ronchi Della Rocca University of Torino
Link to publication DOI
19:10
10m
Talk
Intensional Datatype Refinement
POPL
Eddie Jones University of Bristol, Steven Ramsay University of Bristol
Link to publication DOI
19:20
10m
Talk
Abstracting Gradual Typing Moving Forward : Precise and Space-Efficient
POPL
Felipe Bañados Schwerter University of British Columbia, Alison M. Clark University of British Columbia, Khurram A. Jafery University of British Columbia, Ronald Garcia University 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
Alan Jeffrey Roblox, Lennart Augustsson Epic Games

Fri 22 Jan

Displayed 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 Sherman Massachusetts Institute of Technology, USA, Jesse Michel Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI
15:55
10m
Talk
Deciding Accuracy of Differential Privacy Schemes
POPL
Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Rohit Chadha University of Missouri, Paul Krogmeier University of Illinois at Urbana-Champaign, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI
16:05
10m
Talk
Probabilistic Programming Semantics for Name Generation
POPL
Marcin Sabok McGill University, Sam Staton University of Oxford, Dario Stein University of Oxford, Michael Wolman McGill University
Link to publication DOI Pre-print
16:15
10m
Talk
Simplifying Multiple-Statement Reductions with the Polyhedral Model
POPL
Cambridge Yang MIT CSAIL, Eric Atkinson MIT CSAIL, Michael Carbin Massachusetts Institute of Technology
Link to publication DOI
16:25
10m
Talk
A Pre-Expectation Calculus for Probabilistic SensitivityDistinguished Paper
POPL
Alejandro Aguirre IMDEA Software Institute and T.U. of Madrid (UPM), Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Justin Hsu University of Wisconsin-Madison, USA, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja ETH Zurich
Link to publication DOI
16:35
10m
Talk
Paradoxes of probabilistic programming
POPL
Jules Jacobs Radboud 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 Farka IMDEA Software Institute, Spain, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco Nomadic Labs, Ignacio Fábregas Universidad Complutense de Madrid
Link to publication DOI
15:55
10m
Talk
Transfinite Step-Indexing for Termination
POPL
Simon Spies MPI-SWS and University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge, Derek Dreyer MPI-SWS
Link to publication DOI
16:05
10m
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA, Jovanka Pantović University of Novi Sad, Ivan Prokić University of Novi Sad, Alceste Scalas Technical University of Denmark, Nobuko Yoshida Imperial 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 Gondelman Aarhus University, Simon Oddershede Gregersen Aarhus University, Abel Nieto Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
Link to publication DOI
16:35
10m
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis Kokologiannakis MPI-SWS, Germany, Ilya Kaysin National Research University Higher School of Economics, JetBrains Research, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-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 Benedikt University of Oxford, UK, Pierre Pradic Oxford University
Link to publication DOI
18:40
10m
Talk
Semantics-Guided Synthesis
POPL
Jinwoo Kim University of Wisconsin-Madison, Qinheping Hu University of Wisconsin-Madison, USA, Loris D'Antoni University of Wisconsin-Madison, USA, Thomas Reps University 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 Lee Hanyang 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 Kuperberg LIP, ENS de Lyon, Laureline Pinault LIP, ENS de Lyon, Damien Pous CNRS
Link to publication DOI
18:40
10m
Talk
egg: Fast and Extensible Equality SaturationDistinguished Paper
POPL
Max Willsey University of Washington, USA, Chandrakana Nandi University of Washington, USA, Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Seattle, Pavel Panchekha University of Utah
Link to publication DOI Pre-print
18:50
10m
Talk
Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS
POPL
David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz University 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 Yahav Technion, A: Emery D. Berger University 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