POPL 2024
Sun 14 - Sat 20 January 2024
London, United Kingdom
Toggle navigation
Attending
Venue: Institution of Engineering and Technology
Supporting POPL
Registration
Conference Hotel: Strand Palace Hotel
Information for Virtual Attendees
Information for Presenters
Requesting a Visa
POPL Live Streams
Program
POPL Program
Your Program
Filter by Day
Sun 14 Jan
Mon 15 Jan
Tue 16 Jan
Wed 17 Jan
Thu 18 Jan
Fri 19 Jan
Sat 20 Jan
Tracks
POPL 2024
Artifact Evaluation
Diversity, Equity and Inclusion
POPL
Session Previews
Student Research Competition
Student Volunteers
TutorialFest
Workshops and Co-located Events
Co-hosted Conferences
CPP
VMCAI
Workshops
CoqPL
Dafny
GALOP
Incorrectness
LAFI
N40AI
O'Hearn Fest
PEPM
PLMW @ POPL
PLanQC
POCL
PROPL
PriSC
The Future of Weak Memory
WAW
WITS
Co-hosted Symposia
PADL
Organization
POPL 2024 Committees
Organizing Committee
AV Committee
Student Volunteers
Track Committees
Artifact Evaluation
Diversity, Equity and Inclusion
POPL
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CPP
Organizing Committee
Program Committee
Steering Committee
VMCAI
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Program Committee
Dafny
Program Chairs
Program Committee
Steering Committee
GALOP
Invited Speakers
Organising Committee
Program Committee
Incorrectness
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
N40AI
Organizing Committee
O'Hearn Fest
Program Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PLMW @ POPL
Organizing Committee
Speakers
Panelists
PLanQC
Organizing Committee
Program Committee
POCL
Organizing Committee
Program Committee
PROPL
Chairs
Programme Committee
PriSC
Program Committee
Steering Committee
The Future of Weak Memory
Organizing Committee
Program Committee
WAW
Organizing Committee
WITS
Program Committee
Co-hosted Symposia
PADL
Programme Chairs
Program 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 2024
(
series
) /
Institution of Engineering and Technology
/
Room information: Turing Lecture
Venue
Institution of Engineering and Technology
Room name
Turing Lecture
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) London
.
Use conference time zone: (GMT) London
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-06: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+03: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 14 Jan
Displayed time zone:
London
change
09:00 - 10:30
Applications
Dafny
at
Turing Lecture
Chair(s):
Stefan Zetzsche
Amazon Web Services
09:00
10m
Day opening
Day opening
Dafny
Stefan Zetzsche
Amazon Web Services
,
Joseph Tassarotti
NYU
09:10
60m
Keynote
Verifying a concurrent file system with sequential reasoning
Dafny
Tej Chajed
UW-Madison
10:12
18m
Talk
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Dafny
Alessandro Cimatti
Fondazione Bruno Kessler
,
Alberto Griggio
Fondazione Bruno Kessler
,
Gianluca Redondi
Fondazione Bruno Kessler
11:00 - 12:30
Testing and Teaching / Comparison
Dafny
at
Turing Lecture
Chair(s):
Joseph Tassarotti
NYU
11:00
18m
Talk
Dafny Test Generation
remote
Dafny
Aleksandr Fedchin
Tufts University
,
Jeffrey S. Foster
Tufts University
,
Zvonimir Rakamaric
Amazon Web Services
,
Aaron Tomb
Amazon Web Services
11:18
18m
Talk
Randomised Testing of the Dafny Compiler
Dafny
Alastair F. Donaldson
Imperial College London
,
Dilan Sheth
Imperial College London
,
Jean-Baptiste Tristan
Amazon Web Services
,
Alex Usher
Imperial College London
11:36
18m
Talk
Teaching Logic and Set Theory with Dafny
Dafny
Ran Ettinger
NVIDIA and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan
,
Hezi Daniel
Israel Academic College in Ramat Gan
11:54
18m
Talk
Learn 'em Dafny
Dafny
James Noble
Creative Research & Programming
Pre-print
12:12
18m
Talk
Colouring Flags with Dafny & Idris
Dafny
Jan de Muijnck-Hughes
University of Strathclyde
,
James Noble
Creative Research & Programming
14:00 - 15:30
Proof Stability / Brittleness / Scale
Dafny
at
Turing Lecture
Chair(s):
Stefan Zetzsche
Amazon Web Services
14:00
18m
Talk
Enhancing Proof Stability
Dafny
Sean McLaughlin
Amazon Web Services
,
Georges-Axel Jaloyan
Amazon Web Services
,
Tongtong Xiang
Amazon Web Services
,
Florian Rabe
Amazon Web Services
14:18
18m
Talk
Improving the Stability of Type Safety Proofs in Dafny
Dafny
Joseph W. Cutler
University of Pennsylvania
,
Michael Hicks
Amazon Web Services and the University of Maryland
,
Emina Torlak
Amazon Web Services, USA
14:36
18m
Talk
Incremental Proof Development in Dafny with Module-Based Induction
Dafny
Son Ho
INRIA
,
Clément Pit-Claudel
EPFL
14:54
18m
Talk
Portfolio Solving for Dafny
Dafny
Eric Mugnier
University of California San Diego
,
Sean McLaughlin
Amazon Web Services
,
Aaron Tomb
Amazon Web Services
15:12
18m
Talk
Domesticating Automation
Dafny
Pranav Srinivasan
University of Michigan / VMware Research
,
Oded Padon
VMware Research
,
Jon Howell
VMware Research
,
Andrea Lattuada
VMware Research
16:00 - 17:30
Probabilistic Programs and Testing / Verifying Contracts
Dafny
at
Turing Lecture
Chair(s):
Joseph Tassarotti
NYU
16:00
18m
Talk
VMC: a Dafny Library for Verified Monte Carlo Algorithms
Dafny
Fabian Zaiser
University of Oxford
,
Stefan Zetzsche
Amazon Web Services
,
Jean-Baptiste Tristan
Amazon Web Services
16:18
18m
Talk
Caesar: A Verifier for Probabilistic Programs
Dafny
Philipp Schröer
RWTH Aachen University
,
Kevin Batz
RWTH Aachen University
,
Benjamin Lucien Kaminski
Saarland University; University College London
,
Joost-Pieter Katoen
RWTH Aachen University
,
Christoph Matheja
DTU
16:36
18m
Talk
Verifying Dafny Contract Integrity
Dafny
Cassidy Waldrip
Brigham Young University
,
Eric Mercer
Brigham Young University
16:54
18m
Talk
Testing Specifications In Dafny
Dafny
Eli Goldweber
University Of Michigan
,
Weixin Yu
University Of Michigan
,
Armin Vakil
University Of Michigan
,
Manos Kapritsos
University of Michigan, USA
17:30 - 18:15
Code Generation
Dafny
at
Turing Lecture
Chair(s):
Stefan Zetzsche
Amazon Web Services
17:30
18m
Talk
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Dafny
Christopher Brix
RWTH Aachen University
,
Jean-Baptiste Tristan
Amazon Web Services
17:48
18m
Talk
CLOVER: Closed-Loop Verifiable Code Generation
Dafny
Chuyue Sun
Stanford University
,
Ying Sheng
Stanford University
,
Oded Padon
VMware Research
,
Clark Barrett
Stanford University
18:06
9m
Day closing
Day closing
Dafny
Stefan Zetzsche
Amazon Web Services
,
Joseph Tassarotti
NYU
Mon 15 Jan
Displayed time zone:
London
change
09:00 - 10:30
Session 1
The Future of Weak Memory
at
Turing Lecture
Chair(s):
John Wickerson
Imperial College London
09:00
10m
Talk
Welcome
The Future of Weak Memory
John Wickerson
Imperial College London
,
Azalea Raad
Imperial College London
,
Brijesh Dongol
University of Surrey
,
Mark Batty
University of Kent
,
Peter Sewell
University of Cambridge
09:10
20m
Talk
Some things I wish I hadn’t seen
The Future of Weak Memory
Matthew J. Parkinson
Microsoft Azure Research
09:30
20m
Talk
Heterogeneous concurrency -- a new frontier for weak memory
The Future of Weak Memory
Soham Chakraborty
TU Delft
09:50
20m
Talk
Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Models
The Future of Weak Memory
Vasileios Klimis
Queen Mary University of London
File Attached
10:10
20m
Talk
How Do We Know That Weak Memory Matters?
The Future of Weak Memory
Mike Dodds
Galois, Inc.
File Attached
11:00 - 12:30
Session 2
The Future of Weak Memory
at
Turing Lecture
Chair(s):
John Wickerson
Imperial College London
11:00
22m
Talk
Weak Memory Demands Model-based Compiler Testing
The Future of Weak Memory
Luke Geeson
University College London (UCL)
File Attached
11:22
22m
Talk
On the need for available, functional, and reusable memory models
The Future of Weak Memory
Hernán Ponce de León
Huawei Dresden Research Center
11:45
22m
Talk
What we learned from C++ atomics and memory model standardization
The Future of Weak Memory
Hans-J. Boehm
Google
File Attached
12:07
22m
Talk
Why Languages Should Preserve Load-Store Order
The Future of Weak Memory
Stephen Dolan
Jane Street
14:00 - 15:30
Session 3
The Future of Weak Memory
at
Turing Lecture
Chair(s):
Brijesh Dongol
University of Surrey
14:00
20m
Talk
Compilers should get over themselves and respect semantic dependencies!
The Future of Weak Memory
Paul E. McKenney
14:20
20m
Talk
A case against semantic dependencies
The Future of Weak Memory
Ori Lahav
Tel Aviv University
14:40
20m
Talk
What Compilers desire from Weak Memory Semantics
Remote
The Future of Weak Memory
Akshay Gopalakrishnan
McGill University
File Attached
15:00
20m
Talk
Programmers love mind-bogglingly complicated weak memory models
The Future of Weak Memory
Simon Cooksey
NVIDIA
File Attached
16:00 - 17:30
Session 4
The Future of Weak Memory
at
Turing Lecture
Chair(s):
Brijesh Dongol
University of Surrey
16:00
22m
Talk
Evolving Weak Memory Models for Evolving Architectures
The Future of Weak Memory
Reese Levine
University of California at Santa Cruz
16:22
22m
Talk
In-order execution nails every weak memory behavior
The Future of Weak Memory
Chung-Kil Hur
Seoul National University
16:45
22m
Talk
System-level weak memory models: The need for formalisation, ISA semantics integration and model diversity
The Future of Weak Memory
Thibaut Pérami
University of Cambridge
17:07
22m
Talk
Relaxed systems semantics and how we (hope to) reason above it
The Future of Weak Memory
Ben Simner
Tue 16 Jan
Displayed time zone:
London
change
09:00 - 10:30
First Session
PLMW @ POPL
at
Turing Lecture
09:00
10m
Day opening
Opening
PLMW @ POPL
Derek Dreyer
MPI-SWS
09:10
35m
Social Event
Ice Breaker
PLMW @ POPL
09:45
45m
Talk
The Evolution of Effects
PLMW @ POPL
Nicolas Wu
Imperial College London
11:00 - 12:30
Second Session
PLMW @ POPL
at
Turing Lecture
Chair(s):
Leonidas Lampropoulos
University of Maryland, College Park
11:00
45m
Talk
Refinement Types from Light to Deep Verification
PLMW @ POPL
Niki Vazou
IMDEA Software Institute
11:45
45m
Panel
Panel
PLMW @ POPL
Leonidas Lampropoulos
University of Maryland, College Park
,
Derek Dreyer
MPI-SWS
,
Jules Jacobs
Radboud University Nijmegen
,
Niki Vazou
IMDEA Software Institute
,
Sam Westrick
Carnegie Mellon University
14:00 - 15:30
Third Session
PLMW @ POPL
at
Turing Lecture
Chair(s):
Andrew K. Hirsch
University at Buffalo, SUNY
14:00
45m
Talk
The Potential of Information-Flow Control Research for helping GDPR Compliance
PLMW @ POPL
Alejandro Russo
Chalmers University of Technology, Sweden
14:45
45m
Talk
Consider Collaboration
PLMW @ POPL
Harrison Goldstein
University of Pennsylvania
,
Samantha Frohlich
University of Bristol
16:00 - 17:30
Fourth Session
PLMW @ POPL
at
Turing Lecture
Chair(s):
Hannah Gommerstadt
Vassar College
16:00
45m
Talk
How to Give a Talk
PLMW @ POPL
Neel Krishnaswami
University of Cambridge
16:45
45m
Talk
Managing undergraduate research, as mentor and mentee
PLMW @ POPL
Mae Milano
Princeton University
18:00 - 21:30
Social Event
PLMW @ POPL
at
Turing Lecture
18:00
3h30m
Social Event
Jane Street Board Game Night
PLMW @ POPL
Chris Casinghino
Jane Street
,
Richard A. Eisenberg
Jane Street
Wed 17 Jan
Displayed time zone:
London
change
08:50 - 09:00
Welcome from the Chair
POPL
at
Turing Lecture
10:30 - 11:50
Types 1
POPL
at
Turing Lecture
Chair(s):
Mae Milano
Princeton University
10:30
20m
Talk
Generating Well-Typed Terms that are not "Useless"
POPL
Justin Frank
University of Maryland, College Park
,
Benjamin Quiring
University of Maryland
,
Leonidas Lampropoulos
University of Maryland, College Park
10:50
20m
Talk
Indexed Types for a Statically Safe WebAssembly
POPL
Adam Geller
Computer Science, University of British Columbia
,
Justin Frank
University of Maryland, College Park
,
William J. Bowman
University of British Columbia
DOI
Pre-print
11:10
20m
Talk
The Essence of Generalized Algebraic Data Types
Remote
POPL
Filip Sieczkowski
Heriot-Watt University
,
Sergei Stepanenko
Aarhus University
,
Jonathan Sterling
University of Cambridge
,
Lars Birkedal
Aarhus University
11:30
20m
Talk
Ill-Typed Programs Don't Evaluate
POPL
Steven Ramsay
University of Bristol
,
Charlie Walpole
University of Bristol
13:20 - 14:40
Automated Verification
POPL
at
Turing Lecture
Chair(s):
Gregory Malecha
BedRock Systems
13:20
20m
Talk
Regular Abstractions for Array Systems
POPL
Chih-Duo Hong
National Chengchi University
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
13:40
20m
Talk
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Distinguished Paper
POPL
Neta Elad
Tel Aviv University
,
Oded Padon
VMware Research
,
Sharon Shoham
Tel Aviv University
Link to publication
DOI
14:00
20m
Talk
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Remote
POPL
Jianan Yao
Columbia University
,
Runzhou Tao
Columbia University
,
Ronghui Gu
Columbia University
,
Jason Nieh
Columbia University
14:20
20m
Talk
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Itsaka Rakotonirina
MPI-SP
,
Gilles Barthe
MPI-SP; IMDEA Software Institute
,
Clara Schneidewind
MPI-SP
15:10 - 16:30
Separation Logic
POPL
at
Turing Lecture
Chair(s):
Azalea Raad
Imperial College London
15:10
20m
Talk
An Iris Instance for Verifying CompCert C Programs
POPL
William Mansky
University of Illinois Chicago
,
Ke Du
Pre-print
15:30
20m
Talk
The Logical Essence of Well-Bracketed Control Flow
POPL
Amin Timany
Aarhus University
,
Armaël Guéneau
Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria
,
Lars Birkedal
Aarhus University
15:50
20m
Talk
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
POPL
Simon Oddershede Gregersen
Aarhus University
,
Alejandro Aguirre
Aarhus University
,
Philipp G. Haselwarter
Aarhus University
,
Joseph Tassarotti
NYU
,
Lars Birkedal
Aarhus University
DOI
Pre-print
16:10
20m
Talk
Thunks and Debits in Separation Logic with Time Credits
POPL
François Pottier
Inria
,
Armaël Guéneau
Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria
,
Jacques-Henri Jourdan
CNR, LMF
,
Glen Mével
16:50 - 18:10
Domain-Specific Languages
POPL
at
Turing Lecture
Chair(s):
Satnam Singh
Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun
ShanghaiTech University
,
Fu Song
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China
,
Yuqi Chen
ShanghaiTech University, China
,
Taolue Chen
University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton
Brown University
,
Shriram Krishnamurthi
Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche
Université Paris-Dauphine -- PSL
,
Mohamed-Amine Baazizi
Sorbonne Université
,
Dario Colazzo
Université Paris-Dauphine -- PSL
,
Giorgio Ghelli
Universita di Pisa
,
Carlo Sartiani
Università della Basilicata
,
Stefanie Scherzinger
Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin
The University of Edinburgh
,
Liam O'Connor
University of Edinburgh
,
Rob van Glabbeek
The University of Edinburgh
,
Peter Hoefner
Australian National University
,
Ohad Kammar
University of Edinburgh
,
Michel Steuwer
TU Berlin; University of Edinburgh
Pre-print
Thu 18 Jan
Displayed time zone:
London
change
09:00 - 10:20
Higher-Order Effectful Programs
POPL
at
Turing Lecture
Chair(s):
Sam Lindley
University of Edinburgh
09:00
20m
Talk
On Model-Checking Higher-Order Effectful Programs
POPL
Ugo Dal Lago
University of Bologna & INRIA Sophia Antipolis
,
Alexis Ghyselen
University of Bologna
09:20
20m
Talk
Explicit Effects and Effect Constraints in ReML
POPL
Martin Elsman
University of Copenhagen, Denmark
Link to publication
DOI
09:40
20m
Talk
Decalf: A Directed, Effectful Cost-Aware Logical Framework
POPL
Harrison Grodin
,
Jonathan Sterling
University of Cambridge
,
Yue Niu
Carnegie Mellon University
,
Robert Harper
Carnegie Mellon University
Pre-print
10:00
20m
Talk
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Distinguished Paper
Remote
POPL
Daniel Frumin
University of Groningen
,
Amin Timany
Aarhus University
,
Lars Birkedal
Aarhus University
DOI
Pre-print
10:50 - 12:10
Probabilistic Programs
POPL
at
Turing Lecture
Chair(s):
Jules Jacobs
Radboud University Nijmegen
10:50
20m
Talk
Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
POPL
Nate Ackerman
Harvard University
,
Cameron Freer
Massachusetts Institute of Technology
,
Younesse Kaddar
University of Oxford
,
Jacek Karwowski
University of Oxford
,
Sean Moss
University of Oxford
,
Daniel Roy
University of Toronto
,
Sam Staton
University of Oxford
,
Hongseok Yang
KAIST; IBS
11:10
20m
Talk
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
POPL
Francesca Randone
IMT School for Advanced Studies Lucca
,
Luca Bortolussi
Department of Mathematics and Geosciences, University of Trieste
,
Emilio Incerto
IMT School for Advanced Studies Lucca
,
Mirco Tribastone
IMT Institute for Advanced Studies Lucca, Italy
11:30
20m
Talk
Higher Order Bayesian Networks, Exactly
POPL
Claudia Faggian
Université de Paris & CNRS
,
Daniele Pautasso
Università di Torino
,
Gabriele Vanoni
IRIF, Université Paris Cité
11:50
20m
Talk
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
POPL
Julian Müllner
TU Wien
,
Marcel Moosbrugger
TU Wien
,
Laura Kovács
TU Wien
13:40 - 15:00
Weak Memory and Concurrent Separation Logic
POPL
at
Turing Lecture
Chair(s):
William Mansky
University of Illinois Chicago
13:40
20m
Talk
How Hard is Weak-Memory Testing?
POPL
Soham Chakraborty
TU Delft
,
Shankaranarayanan Krishna
IIT Bombay, India
,
Umang Mathur
National University of Singapore
,
Andreas Pavlogiannis
Aarhus University
Pre-print
14:00
20m
Talk
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
POPL
Angus Hammond
University of Cambridge
,
Zongyuan Liu
Aarhus University
,
Thibaut Pérami
University of Cambridge
,
Peter Sewell
University of Cambridge
,
Lars Birkedal
Aarhus University
,
Jean Pichon-Pharabod
Aarhus University
Pre-print
14:20
20m
Talk
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
POPL
Amin Timany
Aarhus University
,
Simon Oddershede Gregersen
Aarhus University
,
Leo Stefanesco
MPI-SWS
,
Jonas Kastberg Hinrichsen
Aarhus University, Denmark
,
Léon Gondelman
Aarhus University
,
Abel Nieto
Aarhus University
,
Lars Birkedal
Aarhus University
14:40
20m
Talk
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
POPL
Jules Jacobs
Radboud University Nijmegen
,
Jonas Kastberg Hinrichsen
Aarhus University, Denmark
,
Robbert Krebbers
Radboud University Nijmegen
Pre-print
15:30 - 16:50
Algorithmic Verification
POPL
at
Turing Lecture
Chair(s):
Andreas Pavlogiannis
Aarhus University
15:30
20m
Talk
Polyregular functions on unordered trees of bounded height
POPL
Mikolaj Bojanczyk
Warsaw University
,
Bartek Klin
University of Oxford
15:50
20m
Talk
Solving Infinite-State Games via Acceleration
POPL
Philippe Heim
CISPA Helmholtz Center for Information Security
,
Rayna Dimitrova
CISPA Helmholtz Center for Information Security
Pre-print
16:10
20m
Talk
Ramsey Quantifiers in Linear Arithmetics
POPL
Pascal Bergsträßer
University of Kaiserslautern-Landau
,
Moses Ganardi
MPI-SWS
,
Anthony Widjaja Lin
TU Kaiserslautern; MPI-SWS
,
Georg Zetzsche
MPI-SWS
Pre-print
16:30
20m
Talk
Reachability in Continuous Pushdown VASS
POPL
A. R. Balasubramanian
Technical University of Munich
,
Rupak Majumdar
MPI-SWS
,
Ramanathan S. Thinniyam
Uppsala University
,
Georg Zetzsche
MPI-SWS
Pre-print
Fri 19 Jan
Displayed time zone:
London
change
08:50 - 09:00
Welcome
POPL
at
Turing Lecture
08:50
10m
Other
Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process
POPL
Alastair F. Donaldson
Imperial College London
,
John Wickerson
Imperial College London
10:30 - 11:50
Type Theory
POPL
at
Turing Lecture
Chair(s):
Kuen-Bang Hou (Favonia)
University of Minnesota
10:30
20m
Talk
Internal parametricity, without an interval
POPL
Thorsten Altenkirch
University of Nottingham
,
Yorgo Chamoun
École Polytechnique
,
Ambrus Kaposi
Eötvös Loránd University
,
Michael Shulman
University of San Diego
Pre-print
10:50
20m
Talk
Internal and Observational Parametricity for Cubical Agda
POPL
Antoine Van Muylder
KU Leuven
,
Andreas Nuyts
KU Leuven, Belgium
,
Dominique Devriese
KU Leuven
11:10
20m
Talk
Internalizing Indistinguishability with Dependent Types
Remote
POPL
Yiyun Liu
University of Pennsylvania
,
Jonathan Chan
University of Pennsylvania
,
Jessica Shi
University of Pennsylvania
,
Stephanie Weirich
University of Pennsylvania
11:30
20m
Talk
Polynomial Time and Dependent types
POPL
Robert Atkey
University of Strathclyde
13:20 - 14:40
Medley
POPL
at
Turing Lecture
Chair(s):
Xiaokang Qiu
Purdue University
13:20
20m
Talk
Guided Equality Saturation
POPL
Thomas Koehler
INRIA
,
Andrés Goens
University of Amsterdam
,
Siddharth Bhat
the University of Edinburgh
,
Tobias Grosser
University of Edinburgh
,
Phil Trinder
University of Glasgow
,
Michel Steuwer
TU Berlin; University of Edinburgh
Pre-print
13:40
20m
Talk
Fusing Direct Manipulations into Functional Programs
POPL
Xing Zhang
Peking University
,
Ruifeng Xie
Peking University
,
Guanchen Guo
Peking University
,
Xiao He
University of Science and Technology Beijing
,
Tao Zan
Longyan University
,
Zhenjiang Hu
Peking University
Pre-print
14:00
20m
Talk
Inference of Robust Reachability Constraints
POPL
Yanis Sellami
CEA, List, Univ. Grenoble Alpes
,
Guillaume Girol
CEA, List, Université Paris Saclay
,
Frédéric Recoules
CEA, List
,
Damien Couroussé
Univ Grenoble Alpes, CEA, List
,
Sébastien Bardin
CEA LIST, University Paris-Saclay
14:20
20m
Talk
Nominal Recursors as Epi-Recursors
Distinguished Paper
POPL
Andrei Popescu
University of Sheffield
15:10 - 16:30
Mechanized Proofs
POPL
at
Turing Lecture
Chair(s):
Andrei Popescu
University of Sheffield
15:10
20m
Talk
Mechanizing Refinement Types
POPL
Michael Borkowski
University of California, San Diego
,
Niki Vazou
IMDEA Software Institute
,
Ranjit Jhala
University of California at San Diego
15:30
20m
Talk
VST-A: A Foundationally Sound Annotation Verifier
POPL
Litao Zhou
Shanghai Jiao Tong University; University of Hong Kong
,
Jianxing Qin
Shanghai Jiao Tong University
,
Qinshi Wang
Princeton University
,
Andrew W. Appel
Princeton University
,
Qinxiang Cao
Shanghai Jiao Tong University
15:50
20m
Talk
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
POPL
Ling Zhang
Shanghai Jiao Tong University
,
Yuting Wang
Shanghai Jiao Tong University
,
Jinhua Wu
Shanghai Jiao Tong University
,
Jérémie Koenig
Yale University
,
Zhong Shao
Yale University
Pre-print
16:10
20m
Talk
A Formalization of Core Why3 in Coq
POPL
Joshua M. Cohen
Princeton University
,
Philip Johnson-Freyd
Sandia National Laboratories
16:50 - 17:50
Logical Foundations
POPL
at
Turing Lecture
Chair(s):
Emanuele D’Osualdo
MPI-SWS
16:50
20m
Talk
Orthologic with Axioms
POPL
Simon Guilloud
École Polytechnique Fédérale de Lausanne
,
Viktor Kunčak
EPFL, Switzerland
Pre-print
17:10
20m
Talk
Deciding Asynchronous Hyperproperties for Recursive Programs
POPL
Jens Oliver Gutsfeld
Westfälische Wilhelm-Universität Münster (WWU), Germany
,
Markus Müller-Olm
University of Münster
,
Christoph Ohrem
University of Münster
Pre-print
17:30
20m
Talk
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
POPL
Patrick Cousot
New York University
18:10 - 18:15
Farewell from the Chair
POPL
at
Turing Lecture
Sat 20 Jan
Displayed time zone:
London
change
09:00 - 10:30
Session 1
PriSC
at
Turing Lecture
Chair(s):
Marco Patrignani
University of Trento
09:00
5m
Day opening
Introduction
PriSC
Shweta Shinde
ETH Zurich
,
Marco Patrignani
University of Trento
09:05
60m
Keynote
Keynote: Can we reason about the security of concurrent systems code?
PriSC
Peter Sewell
University of Cambridge
10:05
25m
Talk
Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
PriSC
Elias Storme
KU Leuven
,
Sander Huyghebaert
Vrije Universiteit Brussel
,
Steven Keuchel
Vrije Universiteit Brussel
,
Thomas Van Strydonck
KULeuven
,
Dominique Devriese
KU Leuven
File Attached
11:00 - 12:30
Session 2
PriSC
at
Turing Lecture
Chair(s):
Marco Vassena
Utrecht University
11:00
22m
Talk
Microarchitectural Side-Channel Mitigations for Serverless Applications
PriSC
Yayu Wang
The University of British Columbia
,
Aastha Mehta
The University of British Columbia
File Attached
11:22
22m
Talk
Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
PriSC
Xaver Fabian
Cispa Helmholtz Center for Information Security
,
Marco Guarnieri
IMDEA Software Institute
,
Michael Backes
Cispa Helmholtz Center for Information Security
File Attached
11:45
22m
Talk
Secure Composition of SPECTRE Mitigations
PriSC
Matthis Kruse
CISPA Helmholtz Center for Information Security
,
Michael Backes
Cispa Helmholtz Center for Information Security
File Attached
12:07
22m
Talk
When Obfuscations Preserve Cryptographic Constant-Time
PriSC
Matteo Busi
University Ca' Foscari, Venice
,
Pierpaolo Degano
University of Pisa and IMT School for Advanced Studies Lucca
,
Letterio Galletta
IMT School for Advanced Studies Lucca
File Attached
14:00 - 15:30
Session 3
PriSC
at
Turing Lecture
Chair(s):
Matteo Busi
University Ca' Foscari, Venice
14:00
22m
Talk
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
PriSC
Daan Vanoverloop
KU Leuven
,
Hans Winderix
KU Leuven
,
Lesly-Ann Daniel
,
Frank Piessens
KU Leuven
File Attached
14:22
22m
Talk
Modularizing CPU Semantics for Virtualization
PriSC
Paolo G. Giarrusso
BedRock Systems
,
Abhishek Anand
BedRock Systems
,
Gregory Malecha
BedRock Systems
,
František Farka
BedRock Systems
,
Hoang-Hai Dang
BedRock Systems
File Attached
14:45
22m
Talk
All the Binaries Together: A Semantic Approach to Application Binary Interfaces
PriSC
Andrew Wagner
Northeastern University
,
Amal Ahmed
Northeastern University, USA
File Attached
15:07
22m
Talk
Short Talks
PriSC
16:00 - 17:30
Session 4
PriSC
at
Turing Lecture
Chair(s):
Dominique Devriese
KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann
CISPA Helmholtz Center for Information Security
,
Ethan Cecchetti
University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun
Shanghai Jiao Tong University
,
Kunal Singh
Carnegie Mellon University
,
Jan-Paul Ramos-Davila
Cornell University
,
Jonathan Aldrich
Carnegie Mellon University
,
Jenna DiVincenzo (Wise)
Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang
BedRock Systems
,
David Swasey
BedRock Systems
,
Gregory Malecha
BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde
ETH Zurich
Sun 14 Jan
Displayed time zone:
London
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
18:00
30
Turing Lecture
Dafny
Applications
Dafny
Testing and Teaching / Comparison
Dafny
Proof Stability / Brittleness / Scale
Dafny
Probabilistic Programs and Testing / Verifying Contracts
Dafny
Code Generation
Mon 15 Jan
Displayed time zone:
London
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
Turing Lecture
The Future of Weak Memory
Session 1
The Future of Weak Memory
Session 2
The Future of Weak Memory
Session 3
The Future of Weak Memory
Session 4
Tue 16 Jan
Displayed time zone:
London
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
18:00
30
19:00
30
20:00
30
21:00
30
Turing Lecture
PLMW @ POPL
First Session
PLMW @ POPL
Second Session
PLMW @ POPL
Third Session
PLMW @ POPL
Fourth Session
PLMW @ POPL
Social Event
Wed 17 Jan
Displayed time zone:
London
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
Turing Lecture
POPL
Welcome from the Chair
POPL
Types 1
POPL
Automated Verification
POPL
Separation Logic
POPL
Domain-Specific Languages
Thu 18 Jan
Displayed time zone:
London
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
Turing Lecture
POPL
Higher-Order Effectful Programs
POPL
Probabilistic Programs
POPL
Weak Memory and Concurrent Separation Logic
POPL
Algorithmic Verification
Fri 19 Jan
Displayed time zone:
London
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
Turing Lecture
POPL
Welcome
POPL
Type Theory
POPL
Medley
POPL
Mechanized Proofs
POPL
Logical Foundations
POPL
Farewell from the Chair
Sat 20 Jan
Displayed time zone:
London
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
Turing Lecture
PriSC
Session 1
PriSC
Session 2
PriSC
Session 3
PriSC
Session 4
Sun 14 Jan
Displayed time zone:
London
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
Turing Lecture
Dafny
Day opening
09:00 - 09:10
Dafny
Verifying a concurrent file system with sequential reasoning
09:10 - 10:10
Dafny
Towards the verification of a generic interlocking logic: Dafny meets p ...
10:12 - 10:30
Dafny
remote
Dafny Test Generation
11:00 - 11:18
Dafny
Randomised Testing of the Dafny Compiler
11:18 - 11:36
Dafny
Teaching Logic and Set Theory with Dafny
11:36 - 11:54
Dafny
Learn 'em Dafny
11:54 - 12:12
Dafny
Colouring Flags with Dafny & Idris
12:12 - 12:30
Dafny
Enhancing Proof Stability
14:00 - 14:18
Dafny
Improving the Stability of Type Safety Proofs in Dafny
14:18 - 14:36
Dafny
Incremental Proof Development in Dafny with Module-Based Induction
14:36 - 14:54
Dafny
Portfolio Solving for Dafny
14:54 - 15:12
Dafny
Domesticating Automation
15:12 - 15:30
Dafny
VMC: a Dafny Library for Verified Monte Carlo Algorithms
16:00 - 16:18
Dafny
Caesar: A Verifier for Probabilistic Programs
16:18 - 16:36
Dafny
Verifying Dafny Contract Integrity
16:36 - 16:54
Dafny
Testing Specifications In Dafny
16:54 - 17:12
Dafny
Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
17:30 - 17:48
Dafny
CLOVER: Closed-Loop Verifiable Code Generation
17:48 - 18:06
Dafny
Day closing
18:06 - 18:15
Mon 15 Jan
Displayed time zone:
London
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
Turing Lecture
The Future of Weak Memory
Welcome
09:00 - 09:10
The Future of Weak Memory
Some things I wish I hadn’t seen
09:10 - 09:30
The Future of Weak Memory
Heterogeneous concurrency -- a new frontier for weak memory
09:30 - 09:50
The Future of Weak Memory
Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persiste ...
09:50 - 10:10
The Future of Weak Memory
How Do We Know That Weak Memory Matters?
10:10 - 10:30
The Future of Weak Memory
Weak Memory Demands Model-based Compiler Testing
11:00 - 11:22
The Future of Weak Memory
On the need for available, functional, and reusable memory models
11:22 - 11:45
The Future of Weak Memory
What we learned from C++ atomics and memory model standardization
11:45 - 12:07
The Future of Weak Memory
Why Languages Should Preserve Load-Store Order
12:07 - 12:30
The Future of Weak Memory
Compilers should get over themselves and respect semantic dependencies!
14:00 - 14:20
The Future of Weak Memory
A case against semantic dependencies
14:20 - 14:40
The Future of Weak Memory
Remote
What Compilers desire from Weak Memory Semantics
14:40 - 15:00
The Future of Weak Memory
Programmers love mind-bogglingly complicated weak memory models
15:00 - 15:20
The Future of Weak Memory
Evolving Weak Memory Models for Evolving Architectures
16:00 - 16:22
The Future of Weak Memory
In-order execution nails every weak memory behavior
16:22 - 16:45
The Future of Weak Memory
System-level weak memory models: The need for formalisation, ISA semant ...
16:45 - 17:07
The Future of Weak Memory
Relaxed systems semantics and how we (hope to) reason above it
17:07 - 17:30
Tue 16 Jan
Displayed time zone:
London
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
19:00
15
30
45
20:00
15
30
45
21:00
15
30
45
Turing Lecture
PLMW @ POPL
Opening
09:00 - 09:10
PLMW @ POPL
Ice Breaker
09:10 - 09:45
PLMW @ POPL
The Evolution of Effects
09:45 - 10:30
PLMW @ POPL
Refinement Types from Light to Deep Verification
11:00 - 11:45
PLMW @ POPL
Panel
11:45 - 12:30
PLMW @ POPL
The Potential of Information-Flow Control Research for helping GDPR Com ...
14:00 - 14:45
PLMW @ POPL
Consider Collaboration
14:45 - 15:30
PLMW @ POPL
How to Give a Talk
16:00 - 16:45
PLMW @ POPL
Managing undergraduate research, as mentor and mentee
16:45 - 17:30
PLMW @ POPL
Jane Street Board Game Night
18:00 - 21:30
Wed 17 Jan
Displayed time zone:
London
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
18:00
15
30
45
Turing Lecture
POPL
Generating Well-Typed Terms that are not "Useless"
10:30 - 10:50
POPL
Indexed Types for a Statically Safe WebAssembly
10:50 - 11:10
POPL
Remote
The Essence of Generalized Algebraic Data Types
11:10 - 11:30
POPL
Ill-Typed Programs Don't Evaluate
11:30 - 11:50
POPL
Regular Abstractions for Array Systems
13:20 - 13:40
POPL
Distinguished Paper
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Model ...
13:40 - 14:00
POPL
Remote
Mostly Automated Verification of Liveness Properties for Distributed Pr ...
14:00 - 14:20
POPL
Decision and Complexity of Dolev-Yao Hyperproperties
14:20 - 14:40
POPL
An Iris Instance for Verifying CompCert C Programs
15:10 - 15:30
POPL
The Logical Essence of Well-Bracketed Control Flow
15:30 - 15:50
POPL
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
15:50 - 16:10
POPL
Thunks and Debits in Separation Logic with Time Credits
16:10 - 16:30
POPL
EasyBC: A Cryptography-Specific Language for Security Analysis of Block ...
16:50 - 17:10
POPL
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
17:10 - 17:30
POPL
Validation of Modern JSON Schema: Formalization and Complexity
17:30 - 17:50
POPL
Shoggoth - A Formal Foundation for Strategic Rewriting
17:50 - 18:10
Thu 18 Jan
Displayed time zone:
London
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
Turing Lecture
POPL
On Model-Checking Higher-Order Effectful Programs
09:00 - 09:20
POPL
Explicit Effects and Effect Constraints in ReML
09:20 - 09:40
POPL
Decalf: A Directed, Effectful Cost-Aware Logical Framework
09:40 - 10:00
POPL
Distinguished Paper
Remote
Modular Denotational Semantics for Effects with Guarded Interaction Trees
10:00 - 10:20
POPL
Probabilistic programming interfaces for random graphs: Markov categori ...
10:50 - 11:10
POPL
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
11:10 - 11:30
POPL
Higher Order Bayesian Networks, Exactly
11:30 - 11:50
POPL
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Inv ...
11:50 - 12:10
POPL
How Hard is Weak-Memory Testing?
13:40 - 14:00
POPL
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Archit ...
14:00 - 14:20
POPL
Trillium: Higher-Order Concurrent and Distributed Separation Logic for ...
14:20 - 14:40
POPL
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent ...
14:40 - 15:00
POPL
Polyregular functions on unordered trees of bounded height
15:30 - 15:50
POPL
Solving Infinite-State Games via Acceleration
15:50 - 16:10
POPL
Ramsey Quantifiers in Linear Arithmetics
16:10 - 16:30
POPL
Reachability in Continuous Pushdown VASS
16:30 - 16:50
Fri 19 Jan
Displayed time zone:
London
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
Turing Lecture
POPL
Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review ...
08:50 - 09:00
POPL
Internal parametricity, without an interval
10:30 - 10:50
POPL
Internal and Observational Parametricity for Cubical Agda
10:50 - 11:10
POPL
Remote
Internalizing Indistinguishability with Dependent Types
11:10 - 11:30
POPL
Polynomial Time and Dependent types
11:30 - 11:50
POPL
Guided Equality Saturation
13:20 - 13:40
POPL
Fusing Direct Manipulations into Functional Programs
13:40 - 14:00
POPL
Inference of Robust Reachability Constraints
14:00 - 14:20
POPL
Distinguished Paper
Nominal Recursors as Epi-Recursors
14:20 - 14:40
POPL
Mechanizing Refinement Types
15:10 - 15:30
POPL
VST-A: A Foundationally Sound Annotation Verifier
15:30 - 15:50
POPL
Fully Composable and Adequate Verified Compilation with Direct Refineme ...
15:50 - 16:10
POPL
A Formalization of Core Why3 in Coq
16:10 - 16:30
POPL
Orthologic with Axioms
16:50 - 17:10
POPL
Deciding Asynchronous Hyperproperties for Recursive Programs
17:10 - 17:30
POPL
Calculational Design of [In]Correctness Transformational Program Logics ...
17:30 - 17:50
Sat 20 Jan
Displayed time zone:
London
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
Turing Lecture
PriSC
Introduction
09:00 - 09:05
PriSC
Keynote: Can we reason about the security of concurrent systems code?
09:05 - 10:05
PriSC
Secure Calling Conventions for CHERI Capability Machines in Practice (W ...
10:05 - 10:30
PriSC
Microarchitectural Side-Channel Mitigations for Serverless Applications
11:00 - 11:22
PriSC
Lifting Compiler Security Properties to Stronger Attackers: the Specula ...
11:22 - 11:45
PriSC
Secure Composition of SPECTRE Mitigations
11:45 - 12:07
PriSC
When Obfuscations Preserve Cryptographic Constant-Time
12:07 - 12:30
PriSC
Compiler Support for Control-Flow Linearization Using Architectural Mimicry
14:00 - 14:22
PriSC
Modularizing CPU Semantics for Virtualization
14:22 - 14:45
PriSC
All the Binaries Together: A Semantic Approach to Application Binary In ...
14:45 - 15:07
PriSC
Short Talks
15:07 - 15:30
PriSC
Computational-Bounded Robust Compilation and Universally Composable Sec ...
16:00 - 16:22
PriSC
Gradual Verification for Smart Contracts
16:22 - 16:45
PriSC
Towards Modular Specification and Verification of Concurrent Hypervisor ...
16:45 - 17:07
Closing Remarks
17:07 - 17:15
x
Sat 7 Dec 03:53