POPL 2022
Sun 16 - Fri 28 January 2022
Philadelphia, Pennsylvania, United States
Toggle navigation
Attending
Hotel: Westin Philadelphia
Supporting POPL
Accessibility
Visa Information
Registration
Program
POPL Program
Your Program
Filter by Day
Sun 16 Jan
Mon 17 Jan
Tue 18 Jan
Wed 19 Jan
Thu 20 Jan
Fri 21 Jan
Sat 22 Jan
Sun 23 Jan
Mon 24 Jan
Tue 25 Jan
Wed 26 Jan
Thu 27 Jan
Fri 28 Jan
Tracks
POPL 2022
POPL
Student Research Competition
Student Volunteers
TutorialFest
Artifact Evaluation
Workshops and Co-located Events
Virtual Workshop
Diversity, Equity and Inclusion
Co-hosted Conferences
CPP
VMCAI
VMCAI
- Back to the Future: A Fresh Look at Linear Temporal Logic
- Sequential Information Flow
- Simplifying Concurrent Programming via Synchronization Synthesis
Workshops
CoqPL
LAFI
PEPM
PLMW
PriSC
ProLaLa
Programming Languages and the Law
WITS
Co-hosted Symposia
PADL
Organization
POPL 2022 Committees
Organizing Committee
Track Committees
POPL
Student Research Competition
TutorialFest
Artifact Evaluation
Virtual Workshop
Contributors
People Index
Co-hosted Conferences
CPP
Organization Committee
Program Committee
Steering Committee
VMCAI
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Invited speaker
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PLMW
Organizing Committee
Invited speakers
Panelists
PriSC
Program Committee
Steering Committee
ProLaLa
Program Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Programme Committee
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2022
(
series
) /
Westin Philadelphia
/
Room information: Salon III
Venue
Westin Philadelphia
Room name
Salon III
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-05:00) Eastern Time (US & Canada)
.
Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 09:45
Research keynote
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
09:00
45m
Keynote
Research keynote -- Programming Languages and Law: A Research Agenda for a New Field
Remote
ProLaLa
James Grimmelmann
Cornell University
File Attached
09:45 - 10:05
Long talks #1
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
09:45
20m
Talk
Legal Calculi
InPerson
ProLaLa
Shrutarshi Basu
Harvard University
,
Anshuman Mohan
Cornell University
,
James Grimmelmann
Cornell University
,
Nate Foster
Cornell University
File Attached
10:20 - 12:00
Long talks #2
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
10:20
20m
Talk
Position Paper: LLD is All You Need
Remote
ProLaLa
L. Thorne McCarty
Rutgers, The State University of New Jersey
Pre-print
10:40
20m
Talk
Logical English as a Programming Language for the Law
Remote
ProLaLa
Robert Kowalski
Imperial College London
,
Jacinto Dávila
Contratos Lógicos. C.A. and Universidad de Los Andes
,
Miguel Calejo
logicalcontracts.com
File Attached
11:00
20m
Talk
Introduction of PROLEG (PROlog-based LEGal reasoning support system)
Remote
ProLaLa
Ken Satoh
National Institute of Informatics
,
Wachara Fungwacharakorn
National Institute of Informatics
,
Kanae Tsushima
National Institute of Informatics, Japan
File Attached
11:20
20m
Talk
DPCL: a Language Template for Normative Specifications
Remote
ProLaLa
Giovanni Sileno
University of Amsterdam
,
Thomas van Binsbergen
University of Amsterdam
,
Matteo Pascucci
Slovak Academy of Science
,
Tom van Engers
Leibniz Institute / University of Amsterdam / TNO
Pre-print
11:40
20m
Talk
Reflections on the design and application of eFLINT
Remote
ProLaLa
L. Thomas van Binsbergen
CWI
Pre-print
File Attached
13:30 - 14:10
Short talks
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
13:30
10m
Talk
Littleton: An Educational Environment for Property Law
Remote
ProLaLa
Shrutarshi Basu
Harvard University
,
Anshuman Mohan
Cornell University
,
James Grimmelmann
Cornell University
,
Nate Foster
Cornell University
File Attached
13:40
10m
Talk
Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Remote
ProLaLa
Joaquín Arias
Universidad Rey Juan Carlos
,
Mar Moreno-Rebato
Universidad Rey Juan Carlos
,
José Antonio Rodríguez-García
Universidad Rey Juan Carlos
,
Sascha Ossowski
Universidad Rey Juan Carlos
Pre-print
Media Attached
File Attached
13:50
10m
Talk
Probabilistic programming for Employment Tribunal remedies
Remote
ProLaLa
James Cheney
University of Edinburgh; Alan Turing Institute
14:00
10m
Talk
Prevalence of Expression Types in Legislative Text
Remote
ProLaLa
Jason Morris
Service Canada, Lexpedite Legal Technology
14:10 - 14:50
Long talks #3
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
14:10
20m
Talk
Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
Remote
ProLaLa
Corinna Coupette
Max Planck Institute for Informatics, Saarbrücken, Germany
,
Dirk Hartung
Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany
,
Janis Beckedorf
Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany
,
Maximilian Böther
Hasso Plattner Institute, University of Potsdam, Potsdam, Germany
,
Daniel Martin Katz
Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA
Pre-print
File Attached
14:30
20m
Talk
Cod(e)ifying The Law
InPerson
ProLaLa
Nel Escher
University of Michigan
,
Jeffrey Bilik
University of Michigan
,
Alexander Miller
University of Michigan
,
Jennifer Jiyoung Huseby
University of Michigan
,
Divya Ramesh
University of Michigan
,
Alice Liu
University of Michigan
,
Sam Mikell
University of Michigan
,
Nina Cahill
University of Michigan
,
Ben Green
University of Michigan
,
Nikola Banovic
University of Michigan
File Attached
15:05 - 15:25
Long talks #4
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
15:05
20m
Talk
Stipula: a domain specific language for legal contracts
Remote
ProLaLa
Silvia Crafa
University of Padova
,
Cosimo Laneve
University of Bologna
,
Giovanni Sartor
University of Bologna
Pre-print
File Attached
15:25 - 16:10
Industry keynote
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
15:25
45m
Industry talk
Industry keynote -- What does a toolchain for legislation eventually become?
Remote
ProLaLa
Davin Fifield
Oracle
,
Surend Dayal
Australian National University
,
Don Syme
Microsoft
Link to publication
16:10 - 16:30
Long talks #5
ProLaLa
at
Salon III
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
16:10
20m
Talk
Ergo - a programming language for Smart Legal Contracts
Remote
ProLaLa
Niall Roche
Mishcon de Reya,University College London,Accord Project
,
Jerome Simeon
Clause
,
Walter Hernandez
Mishcon de Reya,Accord Project
,
Eason Chen
Accord Project
,
Dan Selman
Docusign,Accord Project
Pre-print
File Attached
16:40 - 17:40
Long talks #6
ProLaLa
at
Salon III
Chair(s):
Shrutarshi Basu
Harvard University
16:40
20m
Talk
A General Library of Legal Components
Remote
ProLaLa
Chris Bailey
University of Illinois College of Law
Link to publication
17:00
20m
Talk
Overview of the CCLAW L4 project
Remote
ProLaLa
Avishkar Mahajan
Singapore Management University
,
Martin Strecker
Singapore Management University
,
Meng Weng Wong
Singapore Management University
17:20
20m
Talk
Turning Catala into a Proof Platform for the Law
Remote
ProLaLa
Alain Delaët
INRIA, ENS Lyon
,
Denis Merigoux
INRIA
,
Aymeric Fromherz
Inria
Pre-print
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
08:50 - 09:00
Welcome from the chairs
CPP
at
Salon III
Chair(s):
Lennart Beringer
Princeton University
,
Robbert Krebbers
Radboud University Nijmegen
,
Andrei Popescu
University of Sheffield
,
Steve Zdancewic
University of Pennsylvania
08:50
10m
Talk
Chairs' report
CPP
File Attached
09:00 - 10:00
Invited Talk
CPP
at
Salon III
Chair(s):
Steve Zdancewic
University of Pennsylvania
09:00
60m
Talk
Coq’s vibrant ecosystem for verification engineering
InPerson
CPP
I:
Andrew W. Appel
Princeton
Link to publication
10:20 - 12:00
Verified Data Structures and Semantics
CPP
at
Salon III
Chair(s):
Jeehoon Kang
KAIST
10:20
25m
Talk
Specification and Verification of a Transient Stack
Distinguished Paper Award
Remote
CPP
Alexandre Moine
Inria
,
Arthur Charguéraud
Inria
,
François Pottier
Inria
DOI
Pre-print
Media Attached
File Attached
10:45
25m
Talk
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
Remote
CPP
Simon Friis Vindum
Aarhus University
,
Lars Birkedal
Aarhus University
,
Daniel Frumin
University of Groningen
Pre-print
Media Attached
11:10
25m
Talk
Applying Formal Verification to Microkernel IPC at Meta
InPerson
CPP
Quentin Carbonneaux
Meta
,
Noam Zilberstein
Cornell University
,
Christoph Klee
Facebook
,
Peter W. O'Hearn
Meta; University College London
,
Francesco Zappa Nardelli
Meta
Pre-print
11:35
25m
Talk
Certified Abstract Machines for Skeletal Semantics
Remote
CPP
Guillaume Ambal
Univ. Rennes
,
Sergueï Lenglet
Université de Lorraine, France
,
Alan Schmitt
Inria
Pre-print
Media Attached
13:30 - 15:10
Semantics and Program Verification
CPP
at
Salon III
Chair(s):
Benjamin Delaware
Purdue University
13:30
25m
Talk
A Compositional Proof Framework for FRETish Requirements
Remote
CPP
Esther Conrad
NASA LaRC
,
Laura Titolo
NIA/NASA LaRC
,
Dimitra Giannakopoulou
NASA Ames Research Center
,
Thomas Pressburger
NASA ARC
,
Aaron Dutle
NASA Langley Research Center
Pre-print
Media Attached
13:55
25m
Talk
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Derivatives
Remote
CPP
Derek Egolf
Northeastern University
,
Sam Lasser
Tufts University
,
Kathleen Fisher
Tufts University
Link to publication
Media Attached
14:20
25m
Talk
Formally Verified Superblock Scheduling
InPerson
CPP
Cyril Six
Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
,
Léo Gourdin
Université Grenoble-Alpes
,
Sylvain Boulmé
Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
,
David Monniaux
CNRS/VERIMAG
,
Justus Fasse
Université Grenoble-Alpes; KU Leuven
,
Nicolas Nardino
École normale supérieure de Lyon
DOI
Pre-print
14:45
25m
Talk
Overcoming Restraint: Composing Verification of Foreign Functions with Cogent
Remote
CPP
Louis Cheung
University of Melbourne
,
Liam O'Connor
University of Edinburgh
,
Christine Rizkallah
University of Melbourne
DOI
Pre-print
Media Attached
15:30 - 17:10
Security and Distributed Systems
CPP
at
Salon III
Chair(s):
Alwyn Goodloe
NASA Langley Research Center
15:30
25m
Talk
Reflection, Rewinding, and Coin-Toss in EasyCrypt
Remote
CPP
Denis Firsov
Tallinn University of Technology
,
Dominique Unruh
University of Tartu
Pre-print
Media Attached
15:55
25m
Talk
A verified algebraic representation of Cairo program execution
Remote
CPP
Jeremy Avigad
Carnegie Mellon University, USA
,
Lior Goldberg
Starkware Industries Ltd.
,
David Levit
Starkware Industries Ltd.
,
Yoav Seginer
cdl-lang.org, Netherlands
,
Alon Titelman
Starkware Industries Ltd.
Pre-print
16:20
25m
Talk
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
InPerson
CPP
William Schultz
Northeastern University
,
Ian Dardik
Northeastern University
,
Stavros Tripakis
Northeastern University
Pre-print
16:45
25m
Talk
Forward build systems, formally
InPerson
CPP
Sarah Spall
Indiana University
,
Neil Mitchell
Meta
,
Sam Tobin-Hochstadt
Indiana University
Link to publication
17:30 - 18:30
Invited Talk
CPP
at
Salon III
Chair(s):
Andrei Popescu
University of Sheffield
17:30
60m
Talk
The seL4 verification: the art and craft of proof and the reality of commercial support
Remote
CPP
I:
June Andronick
Proofcraft, UNSW and seL4 Foundation
Media Attached
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Invited Talk
CPP
at
Salon III
Chair(s):
Laura Titolo
NIA/NASA LaRC
09:00
60m
Talk
Structural Embeddings Revisited
Remote
CPP
I:
Cesar Munoz
AWS
10:20 - 12:00
Proof Infrastructure, Rewriting and Automated Reasoning
CPP
at
Salon III
Chair(s):
Steve Zdancewic
University of Pennsylvania
10:20
25m
Talk
CertiStr: A Certified String Solver
Distinguished Paper Award
Remote
CPP
Shuanglong Kan
TU Kaiserslautern
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
,
Philipp Ruemmer
Uppsala University
,
Micha Schrader
Technische Universität Kaiserslautern
DOI
Pre-print
Media Attached
10:45
25m
Talk
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Remote
CPP
Michael Färber
Universität Innsbruck, Austria
DOI
Pre-print
Media Attached
File Attached
11:10
25m
Talk
An Extension of the Framework Types-To-Sets for Isabelle/HOL
Remote
CPP
Mihails Milehins
Pre-print
Media Attached
11:35
25m
Talk
A Drag-and-Drop Proof Tactic
Remote
CPP
Benjamin Werner
Ecole polytechnique
,
Pablo Donato
Ecole polytechnique
,
Pierre-Yves Strub
Ecole Polytechnique
DOI
Pre-print
Media Attached
13:30 - 15:10
Formalization of Logic, Algebra and Geometry
CPP
at
Salon III
Chair(s):
Andrei Popescu
University of Sheffield
13:30
25m
Talk
Semantic cut elimination for the logic of bunched implications, formalized in Coq
Distinguished Paper Award
Remote
CPP
Daniel Frumin
University of Groningen
Pre-print
Media Attached
13:55
25m
Talk
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq
Remote
CPP
Mark Koch
Saarland University
,
Dominik Kirst
Saarland University
Pre-print
14:20
25m
Talk
Formalising Lie algebras
Remote
CPP
Oliver Nash
Imperial College, London
Pre-print
Media Attached
14:45
25m
Talk
A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
InPerson
CPP
Ariel E. Kellison
Cornell University
Pre-print
15:30 - 16:10
Chairs' Report and Business Meeting
CPP
at
Salon III
Chair(s):
Lennart Beringer
Princeton University
,
Robbert Krebbers
Radboud University Nijmegen
,
Andrei Popescu
University of Sheffield
,
Steve Zdancewic
University of Pennsylvania
15:30
40m
Talk
Chairs' Report
CPP
File Attached
16:30 - 18:10
Category Theory, HoTT, Number Theory
CPP
at
Salon III
Chair(s):
Kuen-Bang Hou (Favonia)
University of Minnesota
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntax
Remote
CPP
Benedikt Ahrens
TU Delft, The Netherlands
,
Ralph Matthes
IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse
,
Anders Mörtberg
Department of Mathematics, Stockholm University
DOI
Pre-print
Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTs
Remote
CPP
Patricia Johann
Appalachian State University
,
Enrico Ghiorzi
Italian Institute of Technology
Pre-print
Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theory
Remote
CPP
Jonathan Prieto-Cubides
University of Bergen
Pre-print
Media Attached
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares Theorem
Remote
CPP
Hing Lun Chan
Australian National University
DOI
Pre-print
Media Attached
File Attached
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
10:20 - 12:00
Separation Logic
POPL
at
Salon III
Chair(s):
James Riely
DePaul University
10:20
25m
Talk
A Separation Logic for Heap Space under Garbage Collection
Remote
POPL
Jean-Marie Madiot
Inria
,
François Pottier
Inria
DOI
Media Attached
10:45
25m
Research paper
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Distinguished Paper
Remote
POPL
Lennard Gäher
MPI-SWS
,
Michael Sammler
MPI-SWS
,
Simon Spies
MPI-SWS
,
Ralf Jung
MPI-SWS
,
Hoang-Hai Dang
MPI-SWS
,
Robbert Krebbers
Radboud University Nijmegen
,
Jeehoon Kang
KAIST
,
Derek Dreyer
MPI-SWS
DOI
Media Attached
11:10
25m
Research paper
Concurrent Incorrectness Separation Logic
Remote
POPL
Azalea Raad
Imperial College London
,
Josh Berdine
Meta
,
Derek Dreyer
MPI-SWS
,
Peter W. O'Hearn
Meta; University College London
DOI
Media Attached
11:35
25m
Research paper
On Incorrectness Logic and Kleene Algebra with Top and Tests
InPerson
POPL
Cheng Zhang
Boston University
,
Arthur Azevedo de Amorim
Boston University
,
Marco Gaboardi
Boston University
DOI
Media Attached
13:30 - 14:45
Weak Memory Models
POPL
at
Salon III
Chair(s):
Mae Milano
University of California, Berkeley
13:30
25m
Research paper
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency
InPerson
POPL
Alan Jeffrey
Roblox
,
James Riely
DePaul University
,
Mark Batty
University of Kent
,
Simon Cooksey
University of Kent
,
Ilya Kaysin
JetBrains Research; University of Cambridge
,
Anton Podkopaev
HSE University
DOI
Media Attached
13:55
25m
Research paper
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal Stores
Remote
POPL
Azalea Raad
Imperial College London
,
Luc Maranget
Inria
,
Viktor Vafeiadis
MPI-SWS
DOI
Media Attached
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order Reduction
Remote
POPL
Michalis Kokologiannakis
MPI-SWS
,
Iason Marmanis
MPI-SWS
,
Vladimir Gladstein
MPI-SWS; St. Petersburg University; JetBrains Research
,
Viktor Vafeiadis
MPI-SWS
DOI
Media Attached
15:05 - 16:20
Concurrency and Parallelism
POPL
at
Salon III
Chair(s):
Andrew Myers
Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot Algorithms
Remote
POPL
Joakim Öhman
IMDEA Software Institute; Universidad Politécnica de Madrid
,
Aleksandar Nanevski
IMDEA Software Institute
DOI
Media Attached
15:30
25m
Research paper
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic
Remote
POPL
Jules Jacobs
Radboud University Nijmegen
,
Stephanie Balzer
Carnegie Mellon University
,
Robbert Krebbers
Radboud University Nijmegen
DOI
Media Attached
15:55
25m
Research paper
Static Prediction of Parallel Computation Graphs
InPerson
POPL
Stefan K. Muller
Illinois Institute of Technology
DOI
Media Attached
16:40 - 17:30
Reasoning about Probabilistic Programs and Algorithms
POPL
at
Salon III
Chair(s):
Armando Solar-Lezama
Massachusetts Institute of Technology
16:40
25m
Research paper
A Separation Logic for Negative Dependence
Remote
POPL
Jialu Bao
Cornell University
,
Marco Gaboardi
Boston University
,
Justin Hsu
Cornell University
,
Joseph Tassarotti
Boston College
DOI
Media Attached
17:05
25m
Research paper
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Remote
POPL
Yizhou Zhang
University of Waterloo
,
Nada Amin
Harvard University
DOI
Media Attached
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
10:20 - 12:00
Quantum Computing
POPL
at
Salon III
Chair(s):
Michael Hicks
University of Maryland at College Park
10:20
25m
Research paper
Quantum Information Effects
Remote
POPL
Chris Heunen
University of Edinburgh
,
Robin Kaarsgaard
University of Edinburgh
DOI
Media Attached
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
InPerson
POPL
Charles Yuan
Massachusetts Institute of Technology
,
Christopher McNally
Massachusetts Institute of Technology
,
Michael Carbin
Massachusetts Institute of Technology
DOI
Media Attached
11:10
25m
Research paper
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic
Remote
POPL
Xuan-Bach Le
Nanyang Technological University
,
Shang-Wei Lin
Nanyang Technological University
,
Jun Sun
Singapore Management University
,
David Sanan
Nanyang Technological University
DOI
Media Attached
11:35
25m
Research paper
Semantics for Variational Quantum Programming
Remote
POPL
Xiaodong Jia
Hunan University
,
Andre Kornell
Tulane University
,
Bert Lindenhovius
JKU Linz
,
Michael Mislove
Tulane University
,
Vladimir Zamdzhiev
Inria
DOI
Media Attached
13:30 - 14:45
Dynamic Analysis
POPL
at
Salon III
Chair(s):
Armando Solar-Lezama
Massachusetts Institute of Technology
13:30
25m
Research paper
A Formal Foundation for Symbolic Evaluation with Merging
Remote
POPL
Sorawee Porncharoenwase
University of Washington
,
Luke Nelson
University of Washington
,
Xi Wang
University of Washington
,
Emina Torlak
University of Washington
DOI
Media Attached
13:55
25m
Research paper
Logarithm and Program Testing
InPerson
POPL
Kuen-Bang Hou (Favonia)
University of Minnesota
,
Zhuyang Wang
University of Minnesota
DOI
Media Attached
14:20
25m
Research paper
Profile Inference Revisited
Remote
POPL
Wenlei He
Facebook
,
Julián Mestre
Facebook; University of Sydney
,
Sergey Pupyrev
,
Lei Wang
Facebook
,
Hongtao Yu
Facebook
DOI
Media Attached
15:05 - 16:20
Metaprogramming
POPL
at
Salon III
Chair(s):
Stephanie Weirich
University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template Haskell
InPerson
POPL
Ningning Xie
University of Toronto
,
Matthew Pickering
Well-Typed LLP
,
Andres Löh
Well-Typed LLP
,
Nicolas Wu
Imperial College London
,
Jeremy Yallop
University of Cambridge
,
Meng Wang
University of Bristol
DOI
Media Attached
15:30
25m
Research paper
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on Itself
Remote
POPL
Junyoung Jang
McGill University
,
Samuel Gélineau
SimSpace
,
Stefan Monnier
Université de Montréal
,
Brigitte Pientka
McGill University
DOI
Media Attached
15:55
25m
Research paper
Type-Level Programming with Match Types
Remote
POPL
Olivier Blanvillain
EPFL
,
Jonathan Immanuel Brachthäuser
University of Tübingen
,
Maxime Kjaer
EPFL
,
Martin Odersky
EPFL
DOI
Media Attached
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
10:20 - 12:00
Semantics 1
POPL
at
Salon III
Chair(s):
Alan Jeffrey
Roblox
10:20
25m
Research paper
From Enhanced Coinduction towards Enhanced Induction
Remote
POPL
Davide Sangiorgi
University of Bologna; Inria
DOI
Media Attached
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets
InPerson
POPL
Delia Kesner
Université de Paris; CNRS; IRIF; Institut Universitaire de France
DOI
Media Attached
11:10
25m
Research paper
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical Relations
Remote
POPL
Ohad Kammar
University of Edinburgh
,
Shin-ya Katsumata
National Institute of Informatics
,
Philip Saville
University of Oxford
DOI
Media Attached
11:35
25m
Research paper
Layered and Object-Based Game Semantics
InPerson
POPL
Arthur Oliveira Vale
Yale University
,
Paul-André Melliès
CNRS; Université de Paris
,
Zhong Shao
Yale University
,
Jérémie Koenig
Yale University
,
Leo Stefanesco
IRIF, University Paris Diderot & CNRS
DOI
Media Attached
13:30 - 14:45
Semantics 2
POPL
at
Salon III
Chair(s):
Marco Gaboardi
Boston University
13:30
25m
Research paper
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
InPerson
POPL
Vikraman Choudhury
Indiana University; University of Cambridge
,
Jacek Karwowski
University of Warsaw
,
Amr Sabry
Indiana University
Link to publication
DOI
Media Attached
13:55
25m
Research paper
A Relational Theory of Effects and Coeffects
Remote
POPL
Ugo Dal Lago
University of Bologna; Inria
,
Francesco Gavazzo
University of Bologna; Inria
DOI
Media Attached
14:20
25m
Research paper
Effectful Program Distancing
Remote
POPL
Ugo Dal Lago
University of Bologna; Inria
,
Francesco Gavazzo
University of Bologna; Inria
DOI
Media Attached
15:05 - 16:20
Type Theory
POPL
at
Salon III
Chair(s):
Kuen-Bang Hou (Favonia)
University of Minnesota
15:05
25m
Research paper
A Cost-Aware Logical Framework
InPerson
POPL
Yue Niu
Carnegie Mellon University
,
Jonathan Sterling
Aarhus University
,
Harrison Grodin
Carnegie Mellon University
,
Robert Harper
Carnegie Mellon University
DOI
Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract Syntax
Distinguished Paper
Remote
POPL
Marcelo Fiore
University of Cambridge
,
Dmitrij Szamozvancev
University of Cambridge
DOI
Media Attached
15:55
25m
Research paper
Observational Equality: Now for Good
Distinguished Paper
Remote
POPL
Loïc Pujet
Inria
,
Nicolas Tabareau
Inria
DOI
Media Attached
16:40 - 17:30
Synthesis
POPL
at
Salon III
Chair(s):
Paul Downen
University of Massachusetts Lowell
16:40
25m
Research paper
Learning Formulas in Finite Variable Logics
Distinguished Paper
InPerson
POPL
Paul Krogmeier
University of Illinois at Urbana-Champaign
,
P. Madhusudan
University of Illinois at Urbana-Champaign
DOI
Media Attached
17:05
25m
Research paper
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Distinguished Paper
Remote
POPL
Anders Miltner
University of Texas at Austin
,
Adrian Trejo Nuñez
University of Texas at Austin
,
Ana Brendel
University of Texas at Austin
,
Swarat Chaudhuri
University of Texas at Austin
,
Işıl Dillig
University of Texas at Austin
DOI
Media Attached
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
09:00 - 10:00
Session 1
WITS
at
Salon III
Chair(s):
Jesper Cockx
TU Delft
,
Richard A. Eisenberg
Tweag
09:00
15m
Talk
CN: A Refinement Type System for C
Remote
WITS
Christopher Pulte
University of Cambridge, UK
,
Dhruv Makwana
University of Cambridge
,
Kayvan Memarian
University of Cambridge
,
Jean Pichon-Pharabod
Aarhus University
,
Peter Sewell
University of Cambridge
,
Neel Krishnaswami
University of Cambridge
09:15
45m
Other
Type-aware equational rewriting (discussion)
In-Person
WITS
Richard A. Eisenberg
Tweag
09:15
45m
Other
Multi case trees: confluence and coverage (discussion)
In-Person
WITS
Tesla Zhang
The Pennsylvania State University
09:15
45m
Other
Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)
Remote
WITS
Syouki Tsuyama
Tokyo Institute of Technology
,
Youyou Cong
Tokyo Institute of Technology
,
Hidehiko Masuhara
Tokyo Institute of Technology
File Attached
09:15
45m
Other
The Expression Problem and Theorem Proving (discussion)
Remote
WITS
Yao Li
University of Pennsylvania
,
Nick Rioux
University of Pennsylvania
,
Stephanie Weirich
University of Pennsylvania
10:20 - 12:00
Session 2
WITS
at
Salon III
Chair(s):
Jesper Cockx
TU Delft
,
Richard A. Eisenberg
Tweag
10:20
45m
Keynote
Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
Remote
WITS
Jonathan Sterling
Aarhus University
11:05
15m
Talk
The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
Remote
WITS
Matthieu Sozeau
Inria
,
Meven Lennon-Bertrand
Inria – LS2N, Université de Nantes
,
Yannick Forster
Inria
11:20
40m
Other
Elaborator reflection APIs (discussion)
Remote
WITS
Jesper Cockx
TU Delft
11:20
40m
Other
Invisible arguments: language design (discussion)
In-Person
WITS
Richard A. Eisenberg
Tweag
13:30 - 14:45
Session 3
WITS
at
Salon III
Chair(s):
Jesper Cockx
TU Delft
,
Richard A. Eisenberg
Tweag
13:30
15m
Talk
Tries that match
Remote
WITS
Sebastian Graf
Karlsruhe Institute of Technology
13:45
15m
Talk
Gotta prove fast: building an ecosystem for effortless native compilation of tactics
Remote
WITS
Sebastian Ullrich
Karlsruhe Institute of Technology
14:00
45m
Other
Benchmarking Binding (discussion)
In-Person
WITS
Stephanie Weirich
University of Pennsylvania
14:00
45m
Other
Fancy module systems (discussion)
Remote
WITS
Jesper Cockx
TU Delft
15:05 - 16:20
Session 4
WITS
at
Salon III
Chair(s):
Jesper Cockx
TU Delft
,
Richard A. Eisenberg
Tweag
15:05
15m
Talk
mitten: A Flexible Multimodal Proof Assistant
Remote
WITS
Philipp Stassen
Aarhus University
,
Daniel Gratzer
Aarhus University
,
Lars Birkedal
Aarhus University
15:20
15m
Talk
Understandable and Useful Error Messages for Liquid Types
Remote
WITS
Alcides Fonseca
LASIGE, Faculdade de Ciências da Universidade de Lisboa
,
Catarina Gamboa
LASIGE, Faculdade de Ciências da Universidade de Lisboa
,
João David
LASIGE, Faculdade de Ciências da Universidade de Lisboa
,
Guilherme Espada
LASIGE, Faculdade de Ciências da Universidade de Lisboa
,
Paulo Canelas
LASIGE, Faculdade de Ciências da Universidade de Lisboa
15:35
15m
Talk
Deciding type equivalence with simple grammars
In-Person
WITS
Bernardo Almeida
LASIGE, Faculty of Sciences, University of Lisbon
,
Andreia Mordido
Lasige / Faculty of Sciences, Universidade de Lisboa
,
Vasco T. Vasconcelos
LASIGE, Faculty of Sciences, University of Lisbon
15:50
15m
Talk
Typechecking up to Congruence
In-Person
WITS
Jad Elkhaleq Ghalayini
University of Cambridge
16:05
15m
Talk
À bas l’η — Coq’s troublesome η-conversion
Remote
WITS
Meven Lennon-Bertrand
Inria – LS2N, Université de Nantes
16:40 - 17:30
Session 5
WITS
at
Salon III
Chair(s):
Jesper Cockx
TU Delft
,
Richard A. Eisenberg
Tweag
16:40
15m
Talk
Using Dependent Types at Scale: Maintaining the Agda Standard Library
In-Person
WITS
Matthew L. Daggitt
Heriot-Watt University
,
Guillaume Allais
University of St Andrews
16:55
15m
Talk
Setting the Record Straight with Singletons
Remote
WITS
Reed Mullanix
University of Minnesota
17:10
15m
Talk
First-class pattern synonyms
In-Person
WITS
Tesla Zhang
The Pennsylvania State University
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon III
ProLaLa
Research keynote
ProLaLa
Long talks #1
ProLaLa
Long talks #2
ProLaLa
Short talks
ProLaLa
Long talks #3
ProLaLa
Long talks #4
ProLaLa
Industry keynote
ProLaLa
Long talks #5
ProLaLa
Long talks #6
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Salon III
CPP
CPP
Welcome from the chairs
CPP
Invited Talk
CPP
CPP
Verified Data Structures and Semantics
CPP
CPP
Semantics and Program Verification
CPP
CPP
Security and Distributed Systems
CPP
CPP
Invited Talk
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Salon III
CPP
CPP
Invited Talk
CPP
CPP
Proof Infrastructure, Rewriting and Automated Reasoning
CPP
CPP
Formalization of Logic, Algebra and Geometry
CPP
CPP
Chairs' Report and Business Meeting
CPP
CPP
Category Theory, HoTT, Number Theory
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon III
POPL
Separation Logic
POPL
Weak Memory Models
POPL
Concurrency and Parallelism
POPL
Reasoning about Probabilistic Programs and Algorithms
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Salon III
POPL
Quantum Computing
POPL
Dynamic Analysis
POPL
Metaprogramming
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon III
POPL
Semantics 1
POPL
Semantics 2
POPL
Type Theory
POPL
Synthesis
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Salon III
WITS
Session 1
WITS
Session 2
WITS
Session 3
WITS
Session 4
WITS
Session 5
Sun 16 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon III
ProLaLa
Remote
Research keynote -- Programming Languages and Law: A Research Agenda fo ...
09:00 - 09:45
ProLaLa
InPerson
Legal Calculi
09:45 - 10:05
ProLaLa
Remote
Position Paper: LLD is All You Need
10:20 - 10:40
ProLaLa
Remote
Logical English as a Programming Language for the Law
10:40 - 11:00
ProLaLa
Remote
Introduction of PROLEG (PROlog-based LEGal reasoning support system)
11:00 - 11:20
ProLaLa
Remote
DPCL: a Language Template for Normative Specifications
11:20 - 11:40
ProLaLa
Remote
Reflections on the design and application of eFLINT
11:40 - 12:00
ProLaLa
Remote
Littleton: An Educational Environment for Property Law
13:30 - 13:40
ProLaLa
Remote
Modeling Administrative Discretion Using Goal-Directed Answer Set Progr ...
13:40 - 13:50
ProLaLa
Remote
Probabilistic programming for Employment Tribunal remedies
13:50 - 14:00
ProLaLa
Remote
Prevalence of Expression Types in Legislative Text
14:00 - 14:10
ProLaLa
Remote
Law Smells: Defining and Detecting Problematic Patterns in Legal Drafting
14:10 - 14:30
ProLaLa
InPerson
Cod(e)ifying The Law
14:30 - 14:50
ProLaLa
Remote
Stipula: a domain specific language for legal contracts
15:05 - 15:25
ProLaLa
Remote
Industry keynote -- What does a toolchain for legislation eventually be ...
15:25 - 16:10
ProLaLa
Remote
Ergo - a programming language for Smart Legal Contracts
16:10 - 16:30
ProLaLa
Remote
A General Library of Legal Components
16:40 - 17:00
ProLaLa
Remote
Overview of the CCLAW L4 project
17:00 - 17:20
ProLaLa
Remote
Turning Catala into a Proof Platform for the Law
17:20 - 17:40
Mon 17 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Salon III
CPP
Chairs' report
08:50 - 09:00
CPP
InPerson
Coq’s vibrant ecosystem for verification engineering
09:00 - 10:00
CPP
Distinguished Paper Award
Remote
Specification and Verification of a Transient Stack
10:20 - 10:45
CPP
Remote
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s ...
10:45 - 11:10
CPP
InPerson
Applying Formal Verification to Microkernel IPC at Meta
11:10 - 11:35
CPP
Remote
Certified Abstract Machines for Skeletal Semantics
11:35 - 12:00
CPP
Remote
A Compositional Proof Framework for FRETish Requirements
13:30 - 13:55
CPP
Remote
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with Deri ...
13:55 - 14:20
CPP
InPerson
Formally Verified Superblock Scheduling
14:20 - 14:45
CPP
Remote
Overcoming Restraint: Composing Verification of Foreign Functions with ...
14:45 - 15:10
CPP
Remote
Reflection, Rewinding, and Coin-Toss in EasyCrypt
15:30 - 15:55
CPP
Remote
A verified algebraic representation of Cairo program execution
15:55 - 16:20
CPP
InPerson
Formal Verification of a Distributed Dynamic Reconfiguration Protocol
16:20 - 16:45
CPP
InPerson
Forward build systems, formally
16:45 - 17:10
CPP
Remote
The seL4 verification: the art and craft of proof and the reality of co ...
17:30 - 18:30
Tue 18 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Salon III
CPP
Remote
Structural Embeddings Revisited
09:00 - 10:00
CPP
Distinguished Paper Award
Remote
CertiStr: A Certified String Solver
10:20 - 10:45
CPP
Remote
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo ...
10:45 - 11:10
CPP
Remote
An Extension of the Framework Types-To-Sets for Isabelle/HOL
11:10 - 11:35
CPP
Remote
A Drag-and-Drop Proof Tactic
11:35 - 12:00
CPP
Distinguished Paper Award
Remote
Semantic cut elimination for the logic of bunched implications, formali ...
13:30 - 13:55
CPP
Remote
Undecidability, Incompleteness, and Completeness of Second-Order Logic ...
13:55 - 14:20
CPP
Remote
Formalising Lie algebras
14:20 - 14:45
CPP
InPerson
A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
14:45 - 15:10
CPP
Chairs' Report
15:30 - 16:10
CPP
Remote
Implementing a category-theoretic framework for typed abstract syntax
16:30 - 16:55
CPP
Remote
(Deep) Induction Rules for GADTs
16:55 - 17:20
CPP
Remote
On homotopy of walks and spherical maps in homotopy type theory
17:20 - 17:45
CPP
Remote
Windmills of the minds: an algorithm for Fermat's Two Squares Theorem
17:45 - 18:10
Wed 19 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon III
POPL
Remote
A Separation Logic for Heap Space under Garbage Collection
10:20 - 10:45
POPL
Distinguished Paper
Remote
Simuliris: A Separation Logic Framework for Verifying Concurrent Progra ...
10:45 - 11:10
POPL
Remote
Concurrent Incorrectness Separation Logic
11:10 - 11:35
POPL
InPerson
On Incorrectness Logic and Kleene Algebra with Top and Tests
11:35 - 12:00
POPL
InPerson
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Me ...
13:30 - 13:55
POPL
Remote
Extending Intel-x86 Consistency and Persistency: Formalising the Semant ...
13:55 - 14:20
POPL
Remote
Truly Stateless, Optimal Dynamic Partial Order Reduction
14:20 - 14:45
POPL
Remote
Visibility Reasoning for Concurrent Snapshot Algorithms
15:05 - 15:30
POPL
Remote
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Sep ...
15:30 - 15:55
POPL
InPerson
Static Prediction of Parallel Computation Graphs
15:55 - 16:20
POPL
Remote
A Separation Logic for Negative Dependence
16:40 - 17:05
POPL
Remote
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual E ...
17:05 - 17:30
Thu 20 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Salon III
POPL
Remote
Quantum Information Effects
10:20 - 10:45
POPL
InPerson
Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
10:45 - 11:10
POPL
Remote
A Quantum Interpretation of Separating Conjunction for Local Reasoning ...
11:10 - 11:35
POPL
Remote
Semantics for Variational Quantum Programming
11:35 - 12:00
POPL
Remote
A Formal Foundation for Symbolic Evaluation with Merging
13:30 - 13:55
POPL
InPerson
Logarithm and Program Testing
13:55 - 14:20
POPL
Remote
Profile Inference Revisited
14:20 - 14:45
POPL
InPerson
Staging with Class: A Specification for Typed Template Haskell
15:05 - 15:30
POPL
Remote
Mœbius: Metaprogramming using Contextual Types: The Stage Where System ...
15:30 - 15:55
POPL
Remote
Type-Level Programming with Match Types
15:55 - 16:20
Fri 21 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon III
POPL
Remote
From Enhanced Coinduction towards Enhanced Induction
10:20 - 10:45
POPL
InPerson
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic ...
10:45 - 11:10
POPL
Remote
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Lo ...
11:10 - 11:35
POPL
InPerson
Layered and Object-Based Game Semantics
11:35 - 12:00
POPL
InPerson
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to R ...
13:30 - 13:55
POPL
Remote
A Relational Theory of Effects and Coeffects
13:55 - 14:20
POPL
Remote
Effectful Program Distancing
14:20 - 14:45
POPL
InPerson
A Cost-Aware Logical Framework
15:05 - 15:30
POPL
Distinguished Paper
Remote
Formal Metatheory of Second-Order Abstract Syntax
15:30 - 15:55
POPL
Distinguished Paper
Remote
Observational Equality: Now for Good
15:55 - 16:20
POPL
Distinguished Paper
InPerson
Learning Formulas in Finite Variable Logics
16:40 - 17:05
POPL
Distinguished Paper
Remote
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Exec ...
17:05 - 17:30
Sat 22 Jan
Displayed time zone:
Eastern Time (US & Canada)
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Salon III
WITS
Remote
CN: A Refinement Type System for C
09:00 - 09:15
WITS
In-Person
Type-aware equational rewriting (discussion)
09:15 - 10:00
In-Person
Multi case trees: confluence and coverage (discussion)
09:15 - 10:00
Remote
Intrinsically-Typed Interpreters for Effectful and Coeffectful Language ...
09:15 - 10:00
Remote
The Expression Problem and Theorem Proving (discussion)
09:15 - 10:00
WITS
Remote
Make Three To Throw Away: Frontiers in Homotopical Proof Assistants
10:20 - 11:05
WITS
Remote
The curious case of case: correct & efficient representation of case an ...
11:05 - 11:20
WITS
Remote
Elaborator reflection APIs (discussion)
11:20 - 12:00
In-Person
Invisible arguments: language design (discussion)
11:20 - 12:00
WITS
Remote
Tries that match
13:30 - 13:45
WITS
Remote
Gotta prove fast: building an ecosystem for effortless native compilati ...
13:45 - 14:00
WITS
In-Person
Benchmarking Binding (discussion)
14:00 - 14:45
Remote
Fancy module systems (discussion)
14:00 - 14:45
WITS
Remote
mitten: A Flexible Multimodal Proof Assistant
15:05 - 15:20
WITS
Remote
Understandable and Useful Error Messages for Liquid Types
15:20 - 15:35
WITS
In-Person
Deciding type equivalence with simple grammars
15:35 - 15:50
WITS
In-Person
Typechecking up to Congruence
15:50 - 16:05
WITS
Remote
À bas l’η — Coq’s troublesome η-conversion
16:05 - 16:20
WITS
In-Person
Using Dependent Types at Scale: Maintaining the Agda Standard Library
16:40 - 16:55
WITS
Remote
Setting the Record Straight with Singletons
16:55 - 17:10
WITS
In-Person
First-class pattern synonyms
17:10 - 17:25
x
Mon 9 Dec 23:06