Turing Lecture - PROPL 2024

VenueInstitution of Engineering and Technology

Room nameTuring Lecture

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT) London.

Use conference time zone: (GMT) LondonSelect other time zone

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 programSpecify 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	ApplicationsDafny 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 / ComparisonDafny at Turing Lecture Chair(s): Joseph Tassarotti NYU

11:00 18m Talk		Dafny Test Generationremote 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 / ScaleDafny 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 ContractsDafny 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 GenerationDafny 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 1The 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 2The 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 3The 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 SemanticsRemote 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 4The 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 SessionPLMW @ 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 SessionPLMW @ 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 SessionPLMW @ 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 SessionPLMW @ 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 EventPLMW @ 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 ChairPOPL at Turing Lecture

10:30 - 11:50	Types 1POPL 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 TypesRemote 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 VerificationPOPL 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 VerificationDistinguished 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 FunctionsRemote 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 LogicPOPL 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 LanguagesPOPL 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 ProgramsPOPL 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 TreesDistinguished PaperRemote POPL Daniel Frumin University of Groningen, Amin Timany Aarhus University, Lars Birkedal Aarhus University DOI Pre-print

10:50 - 12:10	Probabilistic ProgramsPOPL 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 LogicPOPL 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 VerificationPOPL 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	WelcomePOPL 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 TheoryPOPL 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 TypesRemote 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	MedleyPOPL 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-RecursorsDistinguished Paper POPL Andrei Popescu University of Sheffield

15:10 - 16:30	Mechanized ProofsPOPL 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 FoundationsPOPL 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 ChairPOPL at Turing Lecture

Sat 20 Jan
Displayed time zone: London change

09:00 - 10:30	Session 1PriSC 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 2PriSC 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 3PriSC 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 4PriSC 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										Dafnyremote 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 MemoryRemote 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 PaperRemote 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

Room information: Turing Lecture

Program Display Configuration

Sun 14 JanDisplayed time zone: London change

Mon 15 JanDisplayed time zone: London change

Tue 16 JanDisplayed time zone: London change

Wed 17 JanDisplayed time zone: London change

Thu 18 JanDisplayed time zone: London change

Fri 19 JanDisplayed time zone: London change

Sat 20 JanDisplayed time zone: London change

Sun 14 JanDisplayed time zone: London change

Dafny

Dafny

Dafny

Dafny

Dafny

Mon 15 JanDisplayed time zone: London change

The Future of Weak Memory

The Future of Weak Memory

The Future of Weak Memory

The Future of Weak Memory

Tue 16 JanDisplayed time zone: London change

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

PLMW @ POPL

Wed 17 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

POPL

Thu 18 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

Fri 19 JanDisplayed time zone: London change

POPL

POPL

POPL

POPL

POPL

POPL

Sat 20 JanDisplayed time zone: London change

PriSC

PriSC

PriSC

PriSC

Sun 14 JanDisplayed time zone: London change

Mon 15 JanDisplayed time zone: London change

Tue 16 JanDisplayed time zone: London change

Wed 17 JanDisplayed time zone: London change

Thu 18 JanDisplayed time zone: London change

Fri 19 JanDisplayed time zone: London change

Sat 20 JanDisplayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change

Sun 14 Jan
Displayed time zone: London change

Mon 15 Jan
Displayed time zone: London change

Tue 16 Jan
Displayed time zone: London change

Wed 17 Jan
Displayed time zone: London change

Thu 18 Jan
Displayed time zone: London change

Fri 19 Jan
Displayed time zone: London change

Sat 20 Jan
Displayed time zone: London change