You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 15 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Session #1ProLaLa at Kenmore
Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond
09:00
10m
Day opening
Opening comments
ProLaLa
Jonathan Protzenko Microsoft Research, Redmond, Denis Merigoux INRIA, Shrutarshi Basu Middlebury College
09:10
45m
Keynote
Academic keynote : A Logician and Lawyer walk into a Classroom
ProLaLa
Scott Shapiro Yale Law School, Ruzica Piskac Yale University
09:55
25m
Talk
Formal Modeling and Analysis of Legal Contracts using ContractCheck
ProLaLa
Alan Khoja University of Konstanz, Martin Kölbl CertiK, Stefan Leue University of Konstanz, Rüdiger Wilhelmi University of Konstanz
DOI Pre-print
10:20
10m
Talk
What do Relational Properties Have to Say About Legal Expert Systems ?
ProLaLa
Arthur Correnson École Normale Supérieure de Rennes & Saarland University
09:00 - 10:30
First SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
09:00
5m
Day opening
Opening Comments
LAFI
Christine Tasson Sorbonne Université — LIP6, Steven Holtzen Northeastern University
09:05
60m
Keynote
Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning.Boston
LAFI
A: Hongseok Yang KAIST; IBS
10:10
10m
Talk
Exact Inference for Discrete Probabilistic Programs via Generating FunctionsParis
LAFI
A: Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford
File Attached
10:20
10m
Talk
Exact Probabilistic Inference Using Generating FunctionsBoston
LAFI
A: Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University, Mingshuai Chen RWTH Aachen, Joost-Pieter Katoen RWTH Aachen University
File Attached
11:00 - 12:30
Session #2ProLaLa at Kenmore
Chair(s): Shrutarshi Basu Harvard University, Thomas T. Hildebrandt University of Copenhagen, Jonathan Protzenko Microsoft Research, Redmond
11:00
25m
Talk
Building Information Modeling Using Constraint Logic Programming (Extended Abstract)Virtual
ProLaLa
Joaquín Arias Universidad Rey Juan Carlos, Seppo Törmä VisuaLynk Oy, Finland, Manuel Carro IMDEA Software Institute and T.U. of Madrid (UPM), Gopal Gupta University of Texas at Dallas, USA
Link to publication DOI Pre-print File Attached
11:25
25m
Talk
Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming
ProLaLa
Chinmaya Dabral North Carolina State University, Emma Tosch Northeastern University, USA, Chris Martens Northeastern University
Link to publication Pre-print File Attached
11:50
25m
Talk
The Structure and Legal Interpretation of Computer ProgramsVirtual
ProLaLa
James Grimmelmann Cornell University
File Attached
12:15
10m
Talk
Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint
ProLaLa
Sterre Lutz Utrecht University and TNO
DOI Pre-print
12:25
10m
Talk
Defeasible Semantics for L4Virtual
ProLaLa
Guido Governatori Singapore Management University, Meng Weng Wong Singapore Management University
Link to publication DOI
11:00 - 12:30
Second SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
11:00
20m
Talk
What do posterior distributions of probabilistic programs look like?Boston
LAFI
Mathieu Huot University of Oxford, A: Alexander K. Lew Massachusetts Institute of Technology, Vikash K. Mansinghka Massachusetts Institute of Technology, Sam Staton University of Oxford
File Attached
11:20
10m
Talk
Semantics of Probabilistic Program TracesBoston
LAFI
Alexander K. Lew Massachusetts Institute of Technology, A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam, Vikash Mansinghka Massachusetts Institute of Technology
File Attached
11:30
10m
Talk
A convenient category of tracing measure kernelsBoston
LAFI
A: Eli Sennesh Northeastern University, Jan-Willem Van De Meent University of Amsterdam
File Attached
11:45
5m
Talk
Random probability distributions as natural transformationsParis
LAFI
A: Victor Blanchi ENS Paris, Hugo Paquet University of Oxford
File Attached
11:50
5m
Talk
Static Delayed Sampling for Probabilistic Programming LanguagesParis
LAFI
A: Gizem Caylak KTH Royal Institute of Technology, Daniel Lundén KTH Royal Institute of Technology, Viktor Senderov Naturhistoriska riksmuseet, David Broman KTH Royal Institute of Technology
11:55
5m
Talk
Denotational semantics of languages for inference: semirings, monads, and tensorsOnline
LAFI
Cristina Matache University of Edinburgh, A: Sean Moss University of Oxford, Sam Staton University of Oxford, Ariadne Si Suo University of Oxford
12:10
5m
Talk
Separated and Shared Effects in Higher-Order LanguagesBoston
LAFI
A: Pedro Henrique Azevedo de Amorim Cornell University, Justin Hsu Cornell University
12:15
5m
Talk
On Iteration in Discrete Probabilistic ProgrammingBoston
LAFI
A: Mateo Torres-Ruiz , Robin Piedeleu University of Oxford, Alexandra Silva Cornell University, Fabio Zanasi University College London
File Attached
12:20
5m
Talk
Bit-Blasting Probabilistic ProgramsBoston
LAFI
A: Poorva Garg University of California, Los Angeles, Steven Holtzen Northeastern University, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California at Los Angeles
File Attached
12:25
5m
Talk
πMPC: Automatic Security Proofs for MPC ProtocolsBoston
LAFI
A: Mako P. Bates University of Vermont, Joseph P. Near University of Vermont
14:00 - 15:30
Third SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University, Christine Tasson Sorbonne Université — LIP6
14:00
20m
Talk
The Variable Elimination Algorithm as a Let-Term RewritingParis
LAFI
Thomas Ehrhard CNRS and University Paris Diderot, Claudia Faggian Université de Paris & CNRS, A: Michele Pagani IRIF - Université de Paris Cité
14:20
20m
Talk
Contextual source code AD transformations for sum typesOnline
LAFI
Adam Paszke Google Research, A: Gordon Plotkin Google
File Attached
14:45
5m
Talk
Pitfalls of Full Bayesian Inference in Universal Probabilistic ProgrammingOnline
LAFI
A: Tim Reichelt University of Oxford, C.-H. Luke Ong University of Oxford, Tom Rainforth Department of Statistics, University of Oxford
File Attached
14:50
5m
Talk
∂ is for Dialectica: typing differentiable programmingOnline
LAFI
A: Marie Kerjean CNRS, Université Sorbonne Paris Nord, Pierre-Marie Pédrot INRIA
15:00
5m
Talk
On the Reparameterisation Gradient for Non-Differentiable but Continuous ModelsBoston
LAFI
C.-H. Luke Ong NTU, A: Dominik Wagner University of Oxford
File Attached
15:05
5m
Talk
Partial Evaluation of Forward-Mode Automatic DifferentiationBoston
LAFI
A: Oscar Eriksson KTH Royal Institute of Technology, Viktor Palmkvist KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology
15:10
5m
Talk
Distribution Theoretic Semantics for Non-Smooth Differentiable ProgrammingBoston
LAFI
Pedro Henrique Azevedo de Amorim Cornell University, A: Christopher Lam University of Illinois at Urbana-Champaign
15:15
5m
Talk
New foundations for probabilistic separation logicBoston
LAFI
A: John Li Northeastern University, Amal Ahmed Northeastern University, USA, Steven Holtzen Northeastern University
File Attached
15:20
5m
Talk
Verified Reversible Programming for Verified Lossless CompressionBoston
LAFI
A: James Townsend University of Amsterdam, Jan-Willem Van De Meent University of Amsterdam
15:25
5m
Talk
Towards type-driven data-science in Idris
LAFI
Ohad Kammar University of Edinburgh, Katarzyna Marek University of Edinburgh, Minh Nguyen University of Bristol, Michel Steuwer University of Edinburgh, Jacob Walters University of Edinburgh, Robert Wright The University of Edinburgh, UK
16:00 - 18:00
Session #4ProLaLa at Kenmore
Chair(s): Shrutarshi Basu Harvard University, Jonathan Protzenko Microsoft Research, Redmond
16:00
45m
Keynote
Research keynote
ProLaLa
Chris Bailey University of Illinois College of Law
16:45
25m
Talk
Designing an experiment for comparing user interfaces for legal formalization
ProLaLa
Tereza Novotná Masaryk university, Tomer Libal
17:10
10m
Talk
Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as CodeVirtual
ProLaLa
File Attached
17:20
10m
Talk
Formalising Criminal Law in CatalaVirtual
ProLaLa
Luca Arnaboldi The University of Edinburgh, David Aspinall University of Edinburgh, Ronny Bogani University of Edinburgh, Burkhard Schafer University of Edinburgh, Scott Herman Conan & Herman, Jonathan Protzenko Microsoft Research, Redmond, Ekaterina Komendantskaya Heriot-Watt University, UK, Remi Desmartin Heriot-Watt University, Yue Li Heriot-Watt University, UK
Pre-print File Attached
16:00 - 18:00
Poster SessionLAFI at Scollay
Chair(s): Steven Holtzen Northeastern University

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Keynote and contribution paper VMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
09:00
60m
Keynote
Towards a Theoretical Understanding of Property-Directed Reachability
VMCAI
Sharon Shoham Tel Aviv University
10:00
30m
Talk
Distributing and Parallelizing Non-canonical Loops
VMCAI
Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS
09:00 - 10:30
Tutorials 4ATutorialFest at Copley
09:00
90m
Tutorial
Deductive Verification of Probabilistic Programs
TutorialFest
Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
09:00 - 10:30
Tutorials 3ATutorialFest at Kenmore
09:00
90m
Tutorial
QuickChick: Combining Random Testing and Verification in Coq
TutorialFest
Leonidas Lampropoulos University of Maryland, College Park
09:00 - 10:30
Tutorials 2ATutorialFest at Park
09:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
09:00 - 10:30
CompCert and BeyondCPP at Studio 1
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Keynote
CompCert: a journey through the landscape of mechanized semantics for verified compilation
CPP
K: Sandrine Blazy University of Rennes; Inria; CNRS; IRISA
10:08
22m
Talk
Mechanised Semantics for Gated Static Single Assignment
CPP
Yann Herklotz Imperial College London, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA
DOI Pre-print
09:00 - 10:00
Opening & Invited TalkPADL at The Loft
Chair(s): Daniela Inclezan Miami University
09:00
60m
Talk
Towards Declarative Content Generation for Creativity Support Tools
PADL
Chris Martens Northeastern University
10:00 - 10:30
ReasoningPADL at The Loft
Chair(s): Anssi Yli-Jyrä Tampere University
10:00
30m
Talk
Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL
PADL
Haya Majid Qureshi Alpen-Adria-Universität Klagenfurt, Wolfgang Faber University of Klagenfurt
11:00 - 12:30
Static AnalysisVMCAI at Arlington
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
11:00
30m
Talk
Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth
VMCAI
Amir Kafshdar Goharshady IST Austria, Austria, Ahmed Khaled Zaher HKUST
11:30
30m
Talk
Result Invalidation for Incremental Modular Analyses
VMCAI
Jens Van der Plas Software Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel
12:00
30m
Talk
Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
VMCAI
Nicolas Berthier OCamlPro, Narges Khakpour Linnaeus University
11:00 - 12:30
Tutorials 4BTutorialFest at Copley
11:00
90m
Tutorial
Deductive Verification of Probabilistic Programs
TutorialFest
Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU
11:00 - 12:30
Tutorials 3BTutorialFest at Kenmore
11:00
90m
Tutorial
QuickChick: Combining Random Testing and Verification in Coq
TutorialFest
Leonidas Lampropoulos University of Maryland, College Park
11:00 - 12:30
Tutorials 2BTutorialFest at Park
11:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
11:00 - 12:30
Logical FoundationsCPP at Studio 1
Chair(s): Robbert Krebbers Radboud University Nijmegen
11:00
22m
Talk
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systemsdistinguished paper
CPP
Christina Kohl University of Innsbruck, Aart Middeldorp University of Innsbruck
11:22
22m
Talk
Formalizing and computing propositional quantifiersremote presentation
CPP
Hugo Férée Université Paris Cité / IRIF, Sam van Gool Université Paris Cité / IRIF
11:45
22m
Talk
Encoding Dependently-Typed Constructions into Simple Type Theoryremote presentation
CPP
Anthony Bordg University of Cambridge, Adrián Doña Mateo The University of Edinburgh
12:07
22m
Talk
A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
CPP
Yannick Forster Inria, Felix Jahn Saarland University, Gert Smolka Saarland University
11:00 - 12:30
Domain Specific LanguagesPADL at The Loft
Chair(s): Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research
11:00
30m
Talk
Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper)
PADL
Birthe van den Berg KU Leuven, Tom Schrijvers KU Leuven, Peter Dedecker KU Leuven
11:30
30m
Talk
SwitchLog: A Logic Programming Language for Network Switches
PADL
Vaibhav Mehta Princeton University, Devon Loehr Princeton University, John Sonchack University of Pennsylvania, USA, David Walker Princeton University
12:00
30m
Talk
Formalizing and Reasoning about Contracts between Agents
PADL
Dylan Flynn , Chasity Nadeau , Jeannine Shantz , Marcello Balduccini Saint Joseph's University, USA, Tran Cao Son New Mexico State University, Edward Griffor
12:30 - 14:00
14:00 - 15:30
Keynote and best paperVMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
14:00
60m
Keynote
What Can Program Analysis Say About Data Bias?
VMCAI
Aws Albarghouthi University of Wisconsin-Madison
15:00
30m
Talk
Bayesian parameter estimation with guarantees via interval analysis and simulation
VMCAI
Luisa Collodi University of Florence
14:00 - 15:30
Tutorials 8ATutorialFest at Copley
14:00
90m
Tutorial
Neurosymbolic Programming
TutorialFest
Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology
14:00 - 15:30
Tutorials 7ATutorialFest at Kenmore
14:00
90m
Tutorial
RUST: Regions, Uniqueness, Ownership & Types
TutorialFest
James Noble Research & Programming, Tobias Wrigstad Uppsala University, Sweden
Media Attached File Attached
14:00 - 15:30
Tutorials 6ATutorialFest at Park
14:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee
14:00 - 15:30
Tutorials 5ATutorialFest at Scollay
14:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA
14:00 - 15:30
Languages and CompilersCPP at Studio 1
Chair(s): Cody Roux AWS
14:00
22m
Talk
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
CPP
Katherine Kosaian Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, André Platzer Karlsruhe Institute of Technology
14:22
22m
Talk
P4Cub: A Little Language for Big Routers
CPP
Rudy Peterson Cornell University, Eric Campbell Cornell University, John Chen Cornell University, Natalie Isak Microsoft, Calvin Shyu Cornell University, Ryan Doenges Cornell University, Parsia Ataei Cornell University, Nate Foster Cornell University
14:45
22m
Talk
ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
CPP
Haobin Ni Cornell University, Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research
15:07
22m
Talk
Verifying term graph optimizations using Isabelle/HOL
CPP
Brae J. Webb The University of Queensland, Ian J. Hayes The University of Queensland, Mark Utting The University of Queensland
14:00 - 15:30
Applications of Answer Set Programming (I)PADL at The Loft
Chair(s): Wolfgang Faber Alpen-Adria-Universität, Austria
14:00
30m
Talk
Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming
PADL
Zesheng Xu The University of Texas at Dallas, Gopal Gupta University of Texas at Dallas, USA, Elmer Salazar The University of Texas at Dallas, Joaquín Arias Universidad Rey Juan Carlos, Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research
14:30
30m
Talk
Solving Vehicle Equipment Specification Problems with Answer Set Programming
PADL
Raito Takeuchi Nagoya University, Mutsunori Banbara Nagoya University, Naoyuki Tamura Kobe University, JAPAN, Torsten Schaub University of Potsdam
15:00
30m
Talk
Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling
PADL
Anssi Yli-Jyrä Tampere University, Masood Feyzbakhsh Rankooh Tampere University, Tomi Janhunen Tampere University
16:00 - 17:30
Tutorials 8BTutorialFest at Copley
16:00
90m
Tutorial
Neurosymbolic Programming
TutorialFest
Swarat Chaudhuri University of Texas at Austin, Atharva Sehgal University of Texas, Austin, Armando Solar-Lezama Massachusetts Institute of Technology
16:00 - 17:30
Tutorials 7BTutorialFest at Kenmore
16:00
90m
Tutorial
RUST: Regions, Uniqueness, Ownership & Types
TutorialFest
James Noble Research & Programming, Tobias Wrigstad Uppsala University, Sweden
Media Attached File Attached
16:00 - 17:30
Tutorials 6BTutorialFest at Park
16:00
90m
Tutorial
Using a Proof Assistant to Teach PL Theory, Without the Overhead
TutorialFest
Jonathan Aldrich Carnegie Mellon University, John Boyland Univeristy of Wisconsin, Milwaukee
16:00 - 17:30
Tutorials 5BTutorialFest at Scollay
16:00
90m
Tutorial
Incorrectness Logic and Under-approximation: Foundations of Bug Catching
TutorialFest
Quang Loc Le University College London, Peter O'Hearn Facebook, Azalea Raad Imperial College London, Julien Vanegue Bloomberg, USA
16:00 - 18:00
Formalized Mathematics ICPP at Studio 1
Chair(s): Adam Chlipala Massachusetts Institute of Technology
16:00
22m
Talk
Formalising the h-principle and sphere eversionremote presentation
CPP
Patrick Massot , Floris van Doorn University of Pittsburgh, Oliver Nash Imperial College, London
16:22
22m
Talk
A Formalized Reduction of Keller's Conjecture
CPP
Joshua Clune Carnegie Mellon University
16:45
22m
Talk
Computing Cohomology Rings in Cubical Agdadistinguished paper
CPP
Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay, Axel Ljungström Stockholm University, Anders Mörtberg Department of Mathematics, Stockholm University
17:07
8m
Break
short break
CPP

17:15
45m
Meeting
CPP Business Meeting
CPP

Pre-print
16:00 - 17:30
Applications of Answer Set Programming (II)PADL at The Loft
Chair(s): Mutsunori Banbara Nagoya University
16:00
30m
Talk
Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper)
PADL
Denise Angilica Università Della Calabria, Giovambattista Ianni University of Calabria, Italy, Francesco Pacenza Department of Mathematics and Computer Science, University of Calabria, Jessica Zangari Università della Calabria
16:30
30m
Talk
UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper)
PADL
Sarat Chandra Varanasi The University of Texas at Dallas, General Electric Research, Baoluo Meng GE Research, Christopher Alexander GE Research, Szabolcs Borgyos GE Research
17:00
30m
Talk
Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set Programming (Application Paper)
PADL
Ramsha Ali University of Klagenfurt, Mohammed M. S. El-Kholany University of Klagenfurt, Martin Gebser University of Klagenfurt, Austria

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Keynote and contribution paperVMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
09:00
60m
Keynote
Differential Verification of Deep Neural Networks
VMCAI
Chao Wang University of Southern California
10:00
30m
Talk
ARENA: Enhancing Abstract Refinement for Neural Network Verification
VMCAI
Yuyi Zhong , Quang-Trung Ta National University of Singapore, Siau-Cheng Khoo National University of Singapore
09:00 - 10:30
Keynote + 1 talkPEPM at Scollay
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
09:00
60m
Keynote
Fast Cryptographic Code via Partial Evaluation
PEPM
Adam Chlipala Massachusetts Institute of Technology
10:00
30m
Talk
Towards Type Debugging using Partial Evaluation
PEPM
Kanae Tsushima National Institute of Informatics, Japan, Robert Glück University of Copenhagen
09:00 - 10:30
Proof SearchCPP at Studio 1
Chair(s): Brigitte Pientka McGill University
09:00
60m
Keynote
(canceled invited talk)
CPP

10:08
22m
Talk
Aesop: White-Box Best-First Proof Search for Leandistinguished paper
CPP
Jannis Limperg Vrije Universiteit Amsterdam, Asta Halkjær From Technical University of Denmark
Link to publication DOI Pre-print
09:00 - 10:30
Session 1PLMW @ POPL at Studio 2
Chair(s): Hannah Gommerstadt Vassar College
09:00
15m
Talk
Introduction
PLMW @ POPL
Amal Ahmed Northeastern University, USA
Media Attached
09:15
45m
Talk
Imagining the Reader
PLMW @ POPL
Benjamin C. Pierce University of Pennsylvania
Media Attached File Attached
10:00
30m
Social Event
Icebreaker Activity
PLMW @ POPL

09:00 - 10:00
Invited TalkPADL at The Loft
Chair(s): Michael Hanus Kiel University
09:00
60m
Talk
Modern Macros
PADL
Robert Bruce Findler Northwestern University
10:00 - 10:30
DebuggingPADL at The Loft
Chair(s): Steven Libby University of Portland
10:00
30m
Talk
Automatic Rollback Suggestions for Incremental Datalog Evaluation
PADL
David Zhao The University of Sydney, Pavle Subotic Microsoft Azure, Mukund Raghothaman University of Southern California, Bernhard Scholz University of Sydney
11:00 - 12:30
3 talksPEPM at Scollay
Chair(s): Casper Bach Poulsen Delft University of Technology
11:00
30m
Talk
Semantic Transformation Framework for Rewriting Rules
PEPM
Jihee Park KAIST, Jaemin Hong KAIST, Sukyoung Ryu KAIST
11:30
30m
Talk
Symbolic Execution of Hadamard-Toffoli Quantum Circuits
PEPM
Jacques Carette McMaster University, Gerardo Ortiz Indiana University, Amr Sabry Indiana University
12:00
30m
Talk
Generating Programs for Polynomial Multiplication with Correctness Assurance
PEPM
Ryo Tokuda University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba
11:00 - 12:30
Practical ProvingCPP at Studio 1
Chair(s): Dmitriy Traytel University of Copenhagen
11:00
22m
Talk
Terms for Efficient Proof Checking and ParsingRecorded Presentation
CPP
Michael Färber Universität Innsbruck, Austria
11:22
22m
Talk
Compositional pre-processing for automated reasoning in dependent type theoryremote presentation
CPP
Valentin Blot LMF, Inria, Université Paris-Saclay, Denis Cousineau Mitsubishi Electric R&D Centre Europe, Enzo Crance Mitsubishi Electric R&D Centre Europe, Louise Dubois de Prisque LMF, Inria, Université Paris-Saclay, Chantal Keller LRI, Université Paris-Sud, Assia Mahboubi INRIA, Pierre Vial Inria
11:45
22m
Talk
Practical and sound equality tests, automatically
CPP
Benjamin Gregoire INRIA, Jean-Christophe Léchenet Université Côte d’Azur, Inria, Enrico Tassi INRIA
12:07
22m
Talk
Compiling higher-order specifications to SMT solvers: how to deal with rejection constructivelyremote presentation
CPP
Matthew L. Daggitt Heriott-Watt University, Robert Atkey University of Strathclyde, Wen Kokke University of Strathclyde, Ekaterina Komandantskaya Heriot-Watt University, UK, Luca Arnaboldi The University of Edinburgh
11:00 - 12:30
Session 2PLMW @ POPL at Studio 2
Chair(s): Michael Greenberg Stevens Institute of Technology
11:00
45m
Talk
Session Types Meet Polymorphism and Dependent Types
PLMW @ POPL
Peter Thiemann University of Freiburg, Germany
Media Attached File Attached
11:45
45m
Panel
Career Trajectories in PL
PLMW @ POPL
Richard A. Eisenberg Jane Street, Anitha Gollamudi University of Massachusetts Lowell, Ryan Kavanagh McGill University, Joseph Tassarotti NYU, M: Michael Greenberg Stevens Institute of Technology
11:00 - 12:30
Functional (Logic) ProgrammingPADL at The Loft
Chair(s): William E. Byrd University of Alabama at Birmingham, USA
11:00
30m
Talk
RICE: An Optimizing Curry Compiler
PADL
Steven Libby University of Portland
11:30
30m
Talk
Embedding Functional Logic Programming in Haskell via a Compiler Plugin
PADL
Kai-Oliver Prott University of Kiel, Germany, Finn Teegen University of Kiel, Germany, Jan Christiansen Flensburg University of Applied Sciences, Germany
DOI File Attached
12:00
30m
Talk
Program Synthesis Using Example Propagation
PADL
Niek Mulleners Utrecht University, Johan Jeuring Utrecht University, Bastiaan Heeren Open University of the Netherlands, Netherlands
12:30 - 14:00
14:00 - 15:30
Keynote and contribution paperVMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
14:00
60m
Keynote
Verifying, Inferring and Exploiting Code Commutativity
VMCAI
Eric Koskinen Stevens Institute of Technology
14:00 - 15:30
Industry presentation + 1 talkPEPM at Scollay
Chair(s): Sukyoung Ryu KAIST
14:00
60m
Industry talk
MATLAB Coder: Partial Evaluation in Practice
PEPM
Denis Gurchenkov MathWorks, Fred Smith MathWorks
15:00
30m
Talk
Modular Construction of Multi-sorted Free Extensions
PEPM
Guillaume Allais University of St Andrews, Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Nachiappan Valliappan Chalmers University of Technology, Sam Lindley University of Edinburgh, Jeremy Yallop University of Cambridge
File Attached
14:00 - 15:30
ApplicationsCPP at Studio 1
Chair(s): Yoonseung Kim Yale University
14:00
22m
Talk
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Storesremote presentation
CPP
Arvind Arasu Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Aymeric Fromherz Inria, Kesha Hietala University of Maryland, Bryan Parno Carnegie Mellon University, Ravi Ramamurthy Microsoft Research
14:22
22m
Talk
Formalising Decentralised Exchanges in Coq
CPP
Eske Hoy Nielsen Aarhus University, Danil Annenkov Concordium, Bas Spitters Concordium Blockchain Research Center, Aarhus University
14:45
22m
Talk
Semantics of Probabilistic Programs using S-Finite Kernels in Coq
CPP
Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Cyril Cohen Inria, Ayumu Saito Tokyo Institute of Technology
15:07
22m
Talk
Formalising Sharkovsky's Theorem (Proof Pearl)
CPP
Bhavik Mehta University of Cambridge
14:00 - 15:30
VerificationPADL at The Loft
Chair(s): Linda Brodo Università di Sassari
14:00
30m
Talk
Execution Time Program Verification With Tight Bounds
PADL
Ana Carolina Silva FCUP, Manuel Barbosa HASLab - INESC TEC and FCUP, Mario Florido Universidade do Porto
14:30
30m
Talk
From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
PADL
Misaki Kojima Nagoya University, Naoki Nishida Nagoya University
DOI File Attached
15:00
30m
Talk
Multiple Query Satisfiability of Constrained Horn Clauses
PADL
Emanuele De Angelis CNR-IASI, Fabio Fioravanti University of Chieti-Pescara, Alberto Pettorossi University of Rome Tor Vergata, Italy, Maurizio Proietti CNR-IASI
16:00 - 17:30
Model CheckingVMCAI at Arlington
Chair(s): Eric Koskinen Stevens Institute of Technology
16:00
15m
Talk
A Pragmatic Approach to Stateful Partial Order ReductionRecorded
VMCAI
Berk Cirisci IRIF, University Paris Diderot and CNRS, France, Constantin Enea Ecole Polytechnique / LIX / CNRS, Azadeh Farzan University of Toronto, Suha Orhun Mutluergil Sabanci University, Turkey
16:15
15m
Talk
StaticPersist : Compiler Support for PMEM ProgrammingRecorded
VMCAI
Sorav Bansal IIT Delhi and CompilerAI Labs
16:30
30m
Talk
Compositional Verification of Stigmergic Collective Systems
VMCAI
Luca Di Stefano University of Gothenburg, Sweden, Frederic Lang
17:00
30m
Talk
Synthesizing History and Prophecy Variables for Symbolic Model Checking
VMCAI
Cole Vick , Kenneth L. McMillan University of Texas at Austin
16:00 - 17:30
2 online talksPEPM at Scollay
Chair(s): Edwin Brady University of St Andrews, UK
16:00
30m
Talk
Efficient Embedding of Strategic Attribute Grammars via MemoizationRemote
PEPM
José Nuno Macedo University of Minho, Emanuel Rodrigues HASLab & INESC TEC, University of Minho, Marcos Viera University of the Republic, Uruguay, João Saraiva
16:30
30m
Talk
Towards a Reflection for Effect HandlersRecorded
PEPM
Youyou Cong Tokyo Institute of Technology, Kenichi Asai Ochanomizu University
17:00
30m
Day closing
Wrap up
PEPM
Jens Palsberg University of California, Los Angeles (UCLA), Edwin Brady University of St Andrews, UK
16:00 - 17:30
Formalized Mathematics IICPP at Studio 1
Chair(s): Viktor Vafeiadis MPI-SWS
16:00
22m
Talk
A formalization of Doob's martingale convergence theorems in mathlibremote presentation
CPP
Kexing Ying University of Cambridge, Rémy Degenne Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9198-CRIStAL, F-59000 Lille, France
16:22
22m
Talk
A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
CPP
Angeliki Koutsoukou-Argyraki University of Cambridge, Department of Computer Science and Technology, Mantas Bakšys University of Cambridge, Chelsea Edmonds University of Cambridge
16:45
22m
Talk
A Formal Disproof of Hirsch Conjecture
CPP
Xavier Allamigeon Inria and Ecole Polytechnique, Quentin Canu Inria and Ecole Polytechnique, Pierre-Yves Strub Meta
17:07
22m
Talk
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
CPP
Anne Baanen Vrije Universiteit Amsterdam, Alex Best Vrije Universiteit Amsterdam, Nirvana Coppola Vrije Universiteit Amsterdam, Sander R. Dahmen Vrije Universiteit Amsterdam
16:00 - 17:30
Session 4PLMW @ POPL at Studio 2
Chair(s): Robbert Krebbers Radboud University Nijmegen
16:00
45m
Talk
Big Ideas in Program Synthesis
PLMW @ POPL
Nadia Polikarpova University of California at San Diego
Media Attached File Attached
16:45
45m
Talk
Care and Feeding of Advisors
PLMW @ POPL
Stephen Chong Harvard University
Media Attached File Attached
16:00 - 17:30
Analysis and Symbolic MethodsPADL at The Loft
Chair(s): Naoki Nishida Nagoya University
16:00
30m
Talk
Dynamic slicing of Reaction Systems based on assertions and monitors
PADL
Linda Brodo Università di Sassari, Roberto Bruni University of Pisa, Moreno Falaschi Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche, University of Siena
16:30
30m
Talk
Linear Algebraic Abduction with Partial Evaluation
PADL
Tuan Nguyen National Institute of Informatics, Katsumi Inoue NII, Chiaki Sakama Wakayama University
DOI File Attached

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:00 - 09:00
Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B

Career Search

08:30 - 08:50
Wednesday Breakfast Session PreviewSession Previews at White Hill
Chair(s): Nate Foster Cornell University
08:30
10m
Talk
Automated Verification: Session Preview
Session Previews
Michael Greenberg Stevens Institute of Technology
08:40
10m
Talk
Types I: Session Preview
Session Previews
Neel Krishnaswami University of Cambridge
09:00 - 09:10
WelcomePOPL at Grand Ballroom A
Chair(s): Andrew Myers Cornell University, Amal Ahmed Northeastern University, USA
09:10 - 10:15
Invited TalkPOPL at Grand Ballroom A
Chair(s): Amal Ahmed Northeastern University, USA
09:10
65m
Keynote
Principles of Persistent Programming
POPL
10:20 - 10:40
Wednesday Morning Break Session PreviewSession Previews at White Hill
Chair(s): Eric Campbell Cornell University
10:20
10m
Talk
Security: Session Preview
Session Previews
Limin Jia Carnegie Mellon University
10:30
10m
Talk
Synthesis I: Session Preview
Session Previews
Nadia Polikarpova University of California at San Diego
10:45 - 12:00
Types IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:45
25m
Talk
Higher-Order Leak and Deadlock Free LocksDistinguished Paper
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University
DOI
11:10
25m
Talk
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations
POPL
Taro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI
11:35
25m
Talk
Recursive Subtyping for All
POPL
Litao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
10:45 - 12:00
Automated VerificationPOPL at Grand Ballroom A
Chair(s): Michael Greenberg Stevens Institute of Technology
10:45
25m
Talk
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
POPL
Michalis Kokologiannakis MPI-SWS, Ori Lahav Tel Aviv University, Viktor Vafeiadis MPI-SWS
DOI
11:10
25m
Talk
Stratified Commutativity in Verification Algorithms for Concurrent ProgramsVirtual
POPL
Azadeh Farzan University of Toronto, Dominik Klumpp University of Freiburg, Andreas Podelski University of Freiburg
DOI
11:35
25m
Talk
A Partial Order View of Message-Passing Communication Models
POPL
Cinzia Di Giusto Université Côte d'Azur; CNRS, Davide Ferre' Université Côte d'Azur; CNRS, Laetitia Laversa Université Côte d'Azur; CNRS, Etienne Lozes Université Côte d'Azur; CNRS
DOI
12:00 - 13:30
12:00 - 13:30
12:40 - 13:20
Wednesday Lunch Session PreviewSession Previews at White Hill
Chair(s): Chelsea Edmonds University of Cambridge
12:40
10m
Talk
Logic & Decidability I: Session Preview
Session Previews
Zachary Kincaid Princeton University
12:50
10m
Talk
Program Logics & Resources: Session Preview
Session Previews
Philippa Gardner Imperial College London
13:00
10m
Talk
Verified Compilation: Session Preview
Session Previews
Deian Stefan University of California at San Diego
13:10
10m
Talk
Probabilistic Inference: Session Preview
Session Previews
Alexandra Silva Cornell University
13:30 - 14:45
Program Logics & ResourcesPOPL at Avenue34
Chair(s): Robbert Krebbers Radboud University Nijmegen
13:30
25m
Talk
A High-Level Separation Logic for Heap Space under Garbage Collection
POPL
Alexandre Moine Inria, Arthur Charguéraud Inria; Université de Strasbourg; CNRS; ICube, François Pottier Inria
DOI
13:55
25m
Talk
CN: Verifying Systems C Code with Separation-Logic Refinement Types
POPL
Christopher Pulte University of Cambridge, Dhruv C. Makwana University of Cambridge, Thomas Sewell University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
DOI
14:20
25m
Talk
Conditional Contextual Refinement
POPL
Youngju Song Seoul National University; MPI-SWS, Minki Cho Seoul National University, Dongjae Lee Seoul National University, Chung-Kil Hur Seoul National University, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS
DOI
13:30 - 14:45
Logic & Decidability IPOPL at Grand Ballroom A
Chair(s): Zachary Kincaid Princeton University
13:30
25m
Talk
Witnessability of Undecidable Problems
POPL
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI
13:55
25m
Talk
On the Expressive Power of String Constraints
POPL
Joel D. Day Loughborough University, Vijay Ganesh Georgia Tech, Nathan Grewal University of Waterloo, Florin Manea University of Göttingen
DOI
14:20
25m
Talk
A Robust Theory of Series Parallel Graphs
POPL
Rajeev Alur University of Pennsylvania, Caleb Stanford University of California, San Diego; University of California, Davis, Chris Watson University of Pennsylvania
DOI
15:10 - 16:25
SecurityPOPL at Avenue34
Chair(s): Benjamin C. Pierce University of Pennsylvania
15:10
25m
Talk
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
POPL
Alexandra E. Michael University of California at San Diego; University of Washington, Anitha Gollamudi University of Massachusetts Lowell, Jay Bosamiya Carnegie Mellon University, Evan Johnson University of California at San Diego; Arm, Aidan Denlinger University of California at San Diego, Craig Disselkoen University of California at San Diego, Conrad Watt University of Cambridge, Bryan Parno Carnegie Mellon University, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Deian Stefan University of California at San Diego
DOI
15:35
25m
Talk
Reconciling Shannon and Scott with a Lattice of Computable Information
POPL
Sebastian Hunt City University of London, Dave Sands Chalmers University of Technology, Sandro Stucki Amazon Prime Video
Link to publication DOI Pre-print
16:00
25m
Talk
A Core Calculus for Equational Proofs of Cryptographic Protocols
POPL
Joshua Gancher Carnegie Mellon University, Kristina Sojakova Inria, Xiong Fan Rutgers University, Elaine Shi Carnegie Mellon University, Greg Morrisett Cornell University
DOI
15:10 - 16:25
Synthesis IPOPL at Grand Ballroom A
Chair(s): Nadia Polikarpova University of California at San Diego
15:10
25m
Talk
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
POPL
Woosuk Lee Hanyang University, Hangyeol Cho Hanyang University
DOI
15:35
25m
Talk
FlashFill++: Scaling Programming by Example by Cutting to the Chase
POPL
José Pablo Cambronero Microsoft, Sumit Gulwani Microsoft, Vu Le Microsoft, Daniel Perelman Microsoft, Arjun Radhakrishna Microsoft, Clint Simon Microsoft, Ashish Tiwari Microsoft
DOI
16:00
25m
Talk
Unrealizability Logic
POPL
Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison
DOI
16:45 - 18:00
Verified CompilationPOPL at Avenue34
Chair(s): Ralf Jung ETH Zürich
16:45
25m
Talk
DimSum: A Decentralized Approach to Multi-language Semantics and VerificationDistinguished Paper
POPL
Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Youngju Song Seoul National University; MPI-SWS, Emanuele D’Osualdo MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Deepak Garg MPI-SWS, Derek Dreyer MPI-SWS
DOI
17:10
25m
Talk
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
POPL
Aurèle Barrière University of Rennes; Inria; CNRS; IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA, David Pichardie Meta
DOI Pre-print
17:35
25m
Talk
Dargent: A Silver Bullet for Verified Data Layout Refinement
POPL
Zilin Chen UNSW, Ambroise Lafont University of Cambridge, Liam O'Connor University of Edinburgh, Gabriele Keller Utrecht University, Craig McLaughlin UNSW, Vincent Jackson University of Melbourne, Christine Rizkallah University of Melbourne
DOI
16:45 - 18:00
Probabilistic InferencePOPL at Grand Ballroom A
Chair(s): Steven Holtzen Northeastern University
16:45
25m
Talk
Affine Monads and Lazy Structures for Bayesian Programming
POPL
Swaraj Dash University of Oxford, Younesse Kaddar University of Oxford, Hugo Paquet University of Oxford, Sam Staton University of Oxford
DOI
17:10
25m
Talk
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic InferenceVirtual
POPL
Jianlin Li University of Waterloo, Leni Ven University of Waterloo, Pengyuan Shi University of Waterloo, Yizhou Zhang University of Waterloo
DOI
17:35
25m
Talk
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
POPL
Wonyeol Lee Stanford University, Xavier Rival Inria; ENS; CNRS; PSL University, Hongseok Yang KAIST; IBS
DOI
18:00 - 21:00
ReceptionPOPL at Foyer
18:00
3h
Social Event
Reception
POPL

18:00 - 19:30
SRC PosterStudent Research Competition at Grand Ballroom A
Chair(s): Jeehoon Kang KAIST, Danfeng Zhang Pennsylvania State University
18:00
90m
Talk
Zydeco: A Stack-Based Call-By-Push-Value Language
Student Research Competition
Yuchen Jiang University of Michigan, Runze Xue CSE Department at the University of Michigan
18:00
90m
Talk
HasChor: Choreographic Programming in Haskell
Student Research Competition
Gan Shen University of California, Santa Cruz, USA
18:00
90m
Talk
Towards Synthesis in Superposition
Student Research Competition
18:00
90m
Talk
A Formalization of Observational Equivalence in Message Passing Protocols
Student Research Competition
Nathan Liittschwager University of California, Santa Cruz
18:00
90m
Talk
On the metatheory of IRs and the CPS-calculus
Student Research Competition
Paulo Torrens University of Kent
18:00
90m
Talk
Scalable Synthesis of Regular Expressions From Only Positive Examples
Student Research Competition
18:00
90m
Talk
Evaluating Soundness of a Gradual Verifier with Property Based Testing
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
18:00
90m
Talk
A mechanized model for logical clocks
Student Research Competition
Jonathan Castello UC Santa Cruz
18:00
90m
Talk
Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Student Research Competition
Joshua Turcotti Cornell University
18:00
90m
Talk
Synthesizing Vectorized Code via Verified Lifting
Student Research Competition
Jeremy Ferguson University of California-Berkeley
18:00
90m
Talk
Citrus: A Dependently Typed Framework for Pulse-Based Logic
Student Research Competition
Harlan Kringen UC Santa Barbara, Ben Hardekopf University of California at Santa Barbara
18:00
90m
Talk
Neko: A quantum map-filter-reduce programming language
Student Research Competition
Elton Pinto Georgia Institute of Technology
18:00
90m
Talk
Compiling and Running High-level Quantum Programs
Student Research Competition
18:00
90m
Talk
Trace-Guided Inductive Synthesis of Recursive Functional Programs
Student Research Competition
Yongwei Yuan Purdue University
18:10 - 18:30
Wednesday Evening Session PreviewSession Previews at White Hill
Chair(s): Xuejing Huang University of Hong Kong
18:10
10m
Talk
Synthesis II: Session Preview
Session Previews
Nate Foster Cornell University
18:20
10m
Talk
Semantics I: Session Preview
Session Previews
Ugo Dal Lago University of Bologna; Inria

Thu 19 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:00 - 09:00
Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B

Junior Faculty

08:20 - 08:50
Thursday Breakfast Session PreviewSession Previews at White Hill
Chair(s): Eric Campbell Cornell University
08:20
10m
Talk
Program Analysis & Parsing: Session Preview
Session Previews
08:30
10m
Talk
Resource Analysis: Session Preview
Session Previews
Xavier Rival Inria; ENS; CNRS; PSL University
08:40
10m
Talk
Automatic Differentiation: Session Preview
Session Previews
Sasa Misailovic University of Illinois at Urbana-Champaign
09:00 - 10:00
Panel: Next 50 Years of POPLPOPL at Grand Ballroom A
Chair(s): Andrew Myers Cornell University
09:00
60m
Panel
Panel: Next 50 Years of POPL
POPL
M: Derek Dreyer MPI-SWS, P: Michael Carbin Massachusetts Institute of Technology, P: Nate Foster Cornell University, P: Xavier Leroy Collège de France, P: Benjamin C. Pierce University of Pennsylvania, P: Nadia Polikarpova University of California at San Diego, P: Azalea Raad Imperial College London, P: Sharon Shoham Tel Aviv University
10:05 - 10:15
Thursday Morning Break Session PreviewSession Previews at White Hill
Chair(s): Nate Foster Cornell University
10:05
10m
Talk
Type Theory: Session Preview
Session Previews
Max S. New University of Michigan
10:20 - 12:00
Semantics IPOPL at Avenue34
Chair(s): Neel Krishnaswami University of Cambridge
10:20
25m
Talk
A Type-Based Approach to Divide-and-Conquer Recursion in Coq
POPL
Pedro da Costa Abreu Junior Purdue University, Benjamin Delaware Purdue University, Alex Hubers University of Iowa, Christa Jenkins University of Iowa, J. Garrett Morris University of Iowa, Aaron Stump University of Iowa
DOI
10:45
25m
Talk
Elements of Quantitative RewritingVirtual
POPL
Francesco Gavazzo University of Pisa, Cecilia Di Florio University of Bologna
DOI
11:10
25m
Talk
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
POPL
Simon Castellan University of Rennes; Inria; CNRS; IRISA, Pierre Clairambault Université Aix-Marseille; Université de Toulon; CNRS; LIS
DOI
11:35
25m
Talk
Deconstructing the Calculus of Relations with Tape Diagrams
POPL
Filippo Bonchi University of Pisa, Alessandro Di Giorgio University of Pisa, Alessio Santamaria University of Pisa; University of Sussex
DOI
10:20 - 12:00
Synthesis IIPOPL at Grand Ballroom A
Chair(s): Benjamin Delaware Purdue University
10:20
25m
Talk
babble: Learning Better Abstractions with E-Graphs and Anti-unification
POPL
David Cao University of California at San Diego, Rose Kunkel University of California at San Diego, Chandrakana Nandi Certora, Max Willsey University of Washington, Zachary Tatlock University of Washington, Nadia Polikarpova University of California at San Diego
DOI Pre-print
10:45
25m
Talk
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
POPL
Ria Das Stanford University, Joshua B. Tenenbaum Massachusetts Institute of Technology, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Basis; Columbia University
DOI
11:10
25m
Talk
Comparative Synthesis: Learning Near-Optimal Network Designs by Query
POPL
Yanjun Wang Amazon Web Services, USA, Zixuan Li Purdue University, Chuan Jiang Purdue University, Xiaokang Qiu Purdue University, Sanjay Rao Purdue University
DOI
11:35
25m
Talk
Top-Down Synthesis for Library Learning
POPL
Maddy Bowers Massachusetts Institute of Technology, Theo X. Olausson Massachusetts Institute of Technology, Lionel Wong Massachusetts Institute of Technology, Gabriel Grand Massachusetts Institute of Technology, Joshua B. Tenenbaum Massachusetts Institute of Technology, Kevin Ellis Cornell University, Armando Solar-Lezama Massachusetts Institute of Technology
DOI Pre-print
12:00 - 13:30
13:00 - 13:20
Thursday Lunch Session PreviewSession Previews at White Hill
Chair(s): Gabe Grand
13:00
10m
Talk
Logic & Decidability II: Session Preview
Session Previews
Caleb Stanford University of California, San Diego; University of California, Davis
13:10
10m
Talk
Types II: Session Preview
Session Previews
Benjamin C. Pierce University of Pennsylvania
13:30 - 14:45
Resource AnalysisPOPL at Avenue34
Chair(s): Robert Harper Carnegie Mellon University
13:30
25m
Talk
Probabilistic Resource-Aware Session Types
POPL
Ankush Das Amazon, Di Wang Peking University, Jan Hoffmann Carnegie Mellon University
DOI
13:55
25m
Talk
A Calculus for Amortized Expected Runtimes
POPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU, Lena Verscht RWTH Aachen University
DOI
14:20
25m
Talk
A General Noninterference Policy for Polynomial Time
POPL
Emmanuel Hainry Université de Lorraine; CNRS; Inria; LORIA, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA
DOI
13:30 - 14:45
Program Analysis & ParsingPOPL at Grand Ballroom A
Chair(s): David Pichardie Meta
13:30
25m
Talk
SSA Translation Is an Abstract InterpretationDistinguished Paper
POPL
Matthieu Lemerre Université Paris-Saclay - CEA LIST
DOI Pre-print
13:55
25m
Talk
Dynamic Race Detection with O(1) SamplesDistinguished Paper
POPL
Mosaad Al Thokair University of Illinois at Urbana-Champaign, Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
14:20
25m
Talk
Statically Resolvable Ambiguity
POPL
Viktor Palmkvist KTH Royal Institute of Technology, Elias Castegren Uppsala University, Philipp Haller KTH Royal Institute of Technology, David Broman KTH Royal Institute of Technology
DOI
13:30 - 15:00
13:30
15m
Talk
Scalable Synthesis of Regular Expressions From Only Positive Examples
Student Research Competition
13:45
15m
Talk
Synthesizing Vectorized Code via Verified Lifting
Student Research Competition
Jeremy Ferguson University of California-Berkeley
14:00
15m
Talk
Evaluating Soundness of a Gradual Verifier with Property Based Testing
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
14:15
15m
Talk
On the metatheory of IRs and the CPS-calculus
Student Research Competition
Paulo Torrens University of Kent
14:30
15m
Talk
Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Student Research Competition
Joshua Turcotti Cornell University
14:45
15m
Talk
Compiling and Running High-level Quantum Programs
Student Research Competition
15:10 - 16:25
Type TheoryPOPL at Avenue34
Chair(s): Brigitte Pientka McGill University
15:10
25m
Talk
Admissible Types-to-PERs Relativization in Higher-Order LogicDistinguished Paper
POPL
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
DOI
15:35
25m
Talk
An Order-Theoretic Analysis of Universe Polymorphism
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Carlo Angiuli Carnegie Mellon University, Reed Mullanix University of Minnesota
DOI
16:00
25m
Talk
Impredicative Observational Equality
POPL
DOI
15:10 - 16:25
Automatic DifferentiationPOPL at Grand Ballroom A
Chair(s): Ningning Xie Google Brain / University of Toronto
15:10
25m
Talk
You Only Linearize Once: Tangents Transpose to Gradients
POPL
Alexey Radul Google Research, Adam Paszke Google Research, Roy Frostig Google Research, Matthew J. Johnson Google Research, Dougal Maclaurin Google Research
DOI
15:35
25m
Talk
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
POPL
Tom Smeding Utrecht University, Matthijs Vákár Utrecht University
DOI Pre-print
16:00
25m
Talk
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsDistinguished Paper
POPL
Alexander K. Lew Massachusetts Institute of Technology, Mathieu Huot University of Oxford, Sam Staton University of Oxford, Vikash K. Mansinghka Massachusetts Institute of Technology
DOI Pre-print
16:45 - 18:00
POPL Business MeetingPOPL at Grand Ballroom A
18:10 - 18:30
Thursday Evening Session PreviewSession Previews at White Hill
Chair(s): Alexandra E. Michael University of California at San Diego; University of Washington
18:10
10m
Talk
Semantics & Effects: Session Preview
Session Previews
Andrew K. Hirsch University at Buffalo, SUNY
18:20
10m
Talk
Logic Programming: Session Preview
Session Previews
19:30 - 21:30
20:00 - 23:00
URM@POPL Board Game NightDiversity, Equity and Inclusion at Game Night

Fri 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:00 - 09:00
Mentoring BreakfastDiversity, Equity and Inclusion at Grand Ballroom B

SIGPLAN-M

08:30 - 08:50
Friday Breakfast Session PreviewSession Previews at White Hill
Chair(s): Alexandre Moine Inria
08:30
10m
Talk
Formal Methods in Compilation & Implementation: Session Preview
Session Previews
Arjun Guha Northeastern University and Roblox Research
08:40
10m
Talk
Quantum Computing: Session Preview
Session Previews
Jens Palsberg University of California, Los Angeles (UCLA)
09:00 - 10:15
Types IIPOPL at Avenue34
Chair(s): Alan Jeffrey Roblox
09:00
25m
Talk
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
POPL
Nick Rioux University of Pennsylvania, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Steve Zdancewic University of Pennsylvania
DOI
09:25
25m
Talk
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
POPL
Han Xu Peking University, Xuejing Huang University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
DOI
09:50
25m
Talk
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
POPL
Victor Arrial Université Paris Cité - CNRS - IRIF, Giulio Guerrieri Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - Huawei, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France
DOI
09:00 - 10:15
Logic & Decidability IIPOPL at Square
Chair(s): Joost-Pieter Katoen RWTH Aachen University
09:00
25m
Talk
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
POPL
Zachary Kincaid Princeton University, Nicolas Koh Princeton University, Shaowei Zhu Princeton University
DOI
09:25
25m
Talk
Higher-Order MSL Horn Constraints
POPL
Jerome Jochems University of Bristol, Eddie Jones University of Bristol, Steven Ramsay University of Bristol
DOI
09:50
25m
Talk
Fast Coalgebraic Bisimilarity Minimization
POPL
Jules Jacobs Radboud University Nijmegen, Thorsten Wissmann Radboud University Nijmegen
DOI Pre-print
10:20 - 10:40
Friday Morning Break Session PreviewSession Previews at White Hill
Chair(s): Neea Rusch Augusta University
10:20
10m
Talk
Concurrency & Linearizability: Session Preview
Session Previews
Chung-Kil Hur Seoul National University
10:30
10m
Talk
Algorithmic Verification
Session Previews
Umang Mathur National University of Singapore
10:45 - 12:00
Semantics & EffectsPOPL at Avenue34
Chair(s): Stephanie Balzer Carnegie Mellon University
10:45
25m
Talk
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
POPL
Alejandro Aguirre Aarhus University, Lars Birkedal Aarhus University
DOI
11:10
25m
Talk
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
POPL
Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of Pennsylvania
DOI
11:35
25m
Talk
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded
POPL
Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology
DOI Pre-print
10:45 - 12:00
Quantum ComputingPOPL at Square
Chair(s): Ugo Dal Lago University of Bologna; Inria
10:45
25m
Talk
Qunity: A Unified Language for Quantum and Classical Computing
POPL
Finn Voichick University of Maryland, Liyi Li University of Maryland, Robert Rand University of Chicago, Michael Hicks University of Maryland; Amazon
DOI Pre-print
11:10
25m
Talk
Proto-Quipper with Dynamic LiftingVirtual
POPL
Peng Fu Dalhousie University, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University
DOI
11:35
25m
Talk
CoqQ: Foundational Verification of Quantum ProgramsVirtual
POPL
Li Zhou MPI-SP; Institute of Software at Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Pierre-Yves Strub Meta, Junyi Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University
DOI
12:00 - 13:30
12:00 - 13:30
13:00 - 13:20
Friday Lunch Session PreviewSession Previews at White Hill
13:00
10m
Talk
Relational & Automated Verification: Session Preview
Session Previews
Eric Campbell Cornell University
13:10
10m
Talk
Semantics II: Session Preview
Session Previews
Robert Atkey University of Strathclyde
13:30 - 14:45
Formal Methods in Compilation & ImplementationPOPL at Avenue34
Chair(s): Lindsey Kuper University of California at Santa Cruz
13:30
25m
Talk
Tail Recursion Modulo Context: An Equational Approach
POPL
Daan Leijen Microsoft Research, Anton Lorenzen University of Edinburgh
DOI
13:55
25m
Talk
Taking Back Control in an Intermediate Representation for GPU Computing
POPL
Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; Google
DOI
14:20
25m
Talk
Executing Microservice Applications on Serverless, Correctly
POPL
Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of Pennsylvania
DOI
13:30 - 14:45
Logic ProgrammingPOPL at Square
Chair(s): Marco Patrignani University of Trento
13:30
25m
Talk
Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationDistinguished Paper
POPL
Hiroshi Unno University of Tsukuba; RIKEN AIP, Tachio Terauchi Waseda University, Yu Gu University of Tsukuba, Eric Koskinen Stevens Institute of Technology
DOI
13:55
25m
Talk
Optimal CHC Solving via Termination Proofs
POPL
Yu Gu University of Tsukuba, Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI
14:20
25m
Talk
From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
POPL
Aaron Bembenek Harvard University, Michael Greenberg Stevens Institute of Technology, Stephen Chong Harvard University
DOI Pre-print
15:10 - 16:25
Concurrency & LinearizabilityPOPL at Avenue34
Chair(s): Tej Chajed VMware Research
15:10
25m
Talk
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
POPL
Abhishek Kr Singh Tel Aviv University, Ori Lahav Tel Aviv University
DOI
15:35
25m
Talk
The Path to Durable Linearizability
POPL
Emanuele D’Osualdo MPI-SWS, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
DOI
16:00
25m
Talk
A Compositional Theory of Linearizability
POPL
Arthur Oliveira Vale Yale University, Zhong Shao Yale University, Yixuan Chen Yale University
DOI
15:10 - 16:25
Algorithmic VerificationPOPL at Square
Chair(s): Umang Mathur National University of Singapore
15:10
25m
Talk
The Fine-Grained Complexity of CFL Reachability
POPL
Paraschos Koutris University of Wisconsin-Madison, Shaleen Deep Microsoft
DOI
15:35
25m
Talk
Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
POPL
Yuanbo Li Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology, Thomas Reps University of Wisconsin-Madison
DOI
16:00
25m
Talk
Context-Bounded Verification of Context-Free Specifications
POPL
DOI
16:45 - 18:00
Semantics IIPOPL at Avenue34
Chair(s): Max S. New University of Michigan
16:45
25m
Talk
Locally Nameless Sets
POPL
Andrew M. Pitts University of Cambridge
DOI Pre-print
17:10
25m
Talk
Why Are Proofs Relevant in Proof-Relevant Models?
POPL
Axel Kerinec Université Sorbonne Paris Nord; LIPN; CNRS, Giulio Manzonetto Université Sorbonne Paris Nord; LIPN; CNRS, Federico Olimpieri University of Leeds
DOI
17:35
25m
Talk
Towards a Higher-Order Mathematical Operational Semantics
POPL
Sergey Goncharov University of Erlangen-Nuremberg, Stefan Milius University of Erlangen-Nuremberg, Lutz Schröder University of Erlangen-Nuremberg, Stelios Tsampas University of Erlangen-Nuremberg, Henning Urbat University of Erlangen-Nuremberg
DOI Pre-print
16:45 - 18:00
Relational & Automated VerificationPOPL at Square
Chair(s): Christoph Matheja DTU
16:45
25m
Talk
An Algebra of Alignment for Relational Verification
POPL
Timos Antonopoulos Yale University, Eric Koskinen Stevens Institute of Technology, Ton Chanh Le Stevens Institute of Technology, Ramana Nagasamudram Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Minh Ngo Stevens Institute of Technology
DOI
17:10
25m
Talk
Grisette: Symbolic Compilation as a Functional Programming Library
POPL
Sirui Lu University of Washington, Rastislav Bodík Google Research
DOI
17:35
25m
Talk
HFL(Z) Validity Checking for Automated Program Verification
POPL
Naoki Kobayashi University of Tokyo, Kento Tanahashi University of Tokyo, Ryosuke Sato University of Tokyo, Takeshi Tsukada Chiba University
DOI

Sat 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Session 1PriSC at Park
Chair(s): Marco Guarnieri IMDEA Software Institute
09:00
5m
Day opening
Introduction
PriSC

09:05
60m
Keynote
Semantic Intermediate Representations for Sound Language Interoperability
PriSC
Amal Ahmed Northeastern University, USA
Pre-print
10:05
25m
Talk
Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
PriSC
Farzaneh Derakhshan Carnegie Mellon University, Zichao Zhang Carnegie Mellon University, Amit Vasudevan Carnegie Mellon University, Limin Jia Carnegie Mellon University
File Attached
11:00 - 12:30
Session 2PriSC at Park
Chair(s): Cătălin Hriţcu MPI-SP
11:00
25m
Talk
Automated Learning and Verification of Embedded Security Architectures
PriSC
Matteo Busi University Ca' Foscari, Venice, Riccardo Focardi University Ca' Foscari, Venice, Flaminia L. Luccio University Ca' Foscari, Venice
File Attached
11:25
25m
Talk
pi_RA: A pi-calculus for verifying protocols that use remote attestation
PriSC
Emiel Lanckriet KU Leuven, Matteo Busi University Ca' Foscari, Venice, Dominique Devriese KU Leuven
File Attached
11:50
25m
Talk
Robust Constant-Time Cryptography
PriSC
Matthew Kolosick University of California at San Diego, Basavesh Ammanaghatta Shivakumar Max Planck Institute for Security and Privacy (MPI-SP), Sunjay Cauligi University of California at San Diego, USA, Marco Patrignani University of Trento, Marco Vassena Utrecht University, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
Pre-print
12:15
15m
Talk
Short Talk: Generalising secure compilation criteria
PriSC
Emiel Lanckriet KU Leuven
11:00 - 12:30
Session 2CoqPL at Scollay
11:00
30m
Talk
Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
CoqPL
Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Adam Chlipala Massachusetts Institute of Technology
File Attached
11:30
30m
Talk
Integrating graphical proofs in Coq
CoqPL
Pablo Donato Ecole polytechnique, Benjamin Werner LIX, IPP, Kaustuv Chaudhuri INRIA & LIX, IPP
File Attached
12:00
30m
Talk
Towards Formally Verified Path ORAM in Coq
CoqPL
Hannah Leung University of Illinois Urbana-Champaign, Talia Ringer University of Illinois at Urbana-Champaign, Christopher W. Fletcher University of Illinois Urbana-Champaign
File Attached
12:00 - 13:30
LunchPOPL at Avenue34
14:00 - 15:30
Session 3CoqPL at Scollay
14:00
30m
Talk
Verified Differential Privacy for Finite Computers
CoqPL
Vivien Rindisbacher Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University
File Attached
14:30
30m
Talk
Formalizing Monoidal Categories and Actions for Syntax with Binders
CoqPL
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT (CNRS and Univ. of Toulouse), Kobe Wullaert Technical University Delft
File Attached
15:00
30m
Talk
Certifying Complexity Analysis
CoqPL
Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS
File Attached
16:00 - 17:30
Session 4PriSC at Park
Chair(s): Matteo Busi University Ca' Foscari, Venice
16:00
25m
Talk
Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
PriSC
Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego
File Attached
16:25
25m
Talk
FaJITa: Verifying Optimizations on Just-In-Time Programs
PriSC
David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMU
Pre-print File Attached
16:50
25m
Talk
Universally Composable Security for Program Partitioning
PriSC
Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell University
File Attached
16:00 - 17:30
Session with the Coq development teamCoqPL at Scollay
16:00
45m
Talk
Session with the Coq Development Team
CoqPL