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

Sun 16 Jan

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

09:00 - 10:00
KeynoteLAFI at LAFI
Chair(s): Cameron Freer Massachusetts Institute of Technology, Ohad Kammar University of Edinburgh
09:00
60m
Keynote
Abstract types in probabilistic programmingRemote
LAFI
Sam Staton University of Oxford
File Attached
09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Thomas Wies New York University
09:00
60m
Keynote
Sequential Information FlowRemote
VMCAI
Thomas A. Henzinger IST Austria, Austria
09:00 - 09:45
Research keynoteProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:00
45m
Keynote
Research keynote -- Programming Languages and Law: A Research Agenda for a New FieldRemote
ProLaLa
James Grimmelmann Cornell University
File Attached
09:45 - 10:05
Long talks #1ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:45
20m
Talk
Legal CalculiInPerson
ProLaLa
Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University
File Attached
10:20 - 12:00
Invited talksLAFI at LAFI
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:20
33m
Talk
Probabilistic and Differentiable Programming in Scientific SimulatorsRemote
LAFI
Atılım Güneş Baydin Department of Engineering Science, University of Oxford
File Attached
10:53
33m
Talk
Stateful processes in probabilistic programming Remote
LAFI
Hugo Paquet University of Cambridge
File Attached
11:26
33m
Talk
Programming Languages for Automatic Differentiation: What Now?Remote
LAFI
File Attached
10:20 - 11:50
Static Analysis and Abstract InterpretationVMCAI at Salon I
Chair(s): Thomas Wies New York University
10:20
30m
Paper
Relational String Abstract DomainsRemote
VMCAI
Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy
10:50
30m
Paper
Lightweight Shape Analysis based on Physical TypesInPerson
VMCAI
Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris
11:20
30m
Paper
A Flow-Insensitive-Complete Program RepresentationRemote
VMCAI
Solène Mirliaz ENS Rennes / IRISA / Inria, David Pichardie Facebook Paris
10:20 - 12:00
Long talks #2ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
10:20
20m
Talk
Position Paper: LLD is All You NeedRemote
ProLaLa
L. Thorne McCarty Rutgers, The State University of New Jersey
Pre-print
10:40
20m
Talk
Logical English as a Programming Language for the LawRemote
ProLaLa
Robert Kowalski Imperial College London, Jacinto Dávila Contratos Lógicos. C.A. and Universidad de Los Andes, Miguel Calejo logicalcontracts.com
File Attached
11:00
20m
Talk
Introduction of PROLEG (PROlog-based LEGal reasoning support system)Remote
ProLaLa
Ken Satoh National Institute of Informatics, Wachara Fungwacharakorn National Institute of Informatics, Kanae Tsushima National Institute of Informatics, Japan
File Attached
11:20
20m
Talk
DPCL: a Language Template for Normative SpecificationsRemote
ProLaLa
Giovanni Sileno University of Amsterdam, Thomas van Binsbergen University of Amsterdam, Matteo Pascucci Slovak Academy of Science, Tom van Engers Leibniz Institute / University of Amsterdam / TNO
Pre-print
11:40
20m
Talk
Reflections on the design and application of eFLINTRemote
ProLaLa
Pre-print File Attached
13:30 - 14:30
Privacy and SecurityVMCAI at Salon I
Chair(s): Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences
13:30
30m
Paper
Verifying Pufferfish Privacy in Hidden Markov ModelsRemote
VMCAI
Depeng Liu Institute of Software, Chinese Academy of Sciences, Bow-Yaw Wang Academia Sinica, Lijun Zhang Institute of Software, Chinese Academy of Sciences
14:00
30m
Paper
Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACERemote
VMCAI
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo
13:30 - 14:10
Short talksProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
13:30
10m
Talk
Littleton: An Educational Environment for Property LawRemote
ProLaLa
Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University
File Attached
13:40
10m
Talk
Modeling Administrative Discretion Using Goal-Directed Answer Set ProgrammingRemote
ProLaLa
Joaquín Arias Universidad Rey Juan Carlos, Mar Moreno-Rebato Universidad Rey Juan Carlos, José Antonio Rodríguez-García Universidad Rey Juan Carlos, Sascha Ossowski Universidad Rey Juan Carlos
Pre-print Media Attached File Attached
13:50
10m
Talk
Probabilistic programming for Employment Tribunal remediesRemote
ProLaLa
James Cheney University of Edinburgh; Alan Turing Institute
14:00
10m
Talk
Prevalence of Expression Types in Legislative TextRemote
ProLaLa
Jason Morris Service Canada, Lexpedite Legal Technology
14:10 - 14:50
Long talks #3ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
14:10
20m
Talk
Law Smells: Defining and Detecting Problematic Patterns in Legal DraftingRemote
ProLaLa
Corinna Coupette Max Planck Institute for Informatics, Saarbrücken, Germany, Dirk Hartung Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany, Janis Beckedorf Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany, Maximilian Böther Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Daniel Martin Katz Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA
Pre-print File Attached
14:30
20m
Talk
Cod(e)ifying The LawInPerson
ProLaLa
Nel Escher University of Michigan, Jeffrey Bilik University of Michigan, Alexander Miller University of Michigan, Jennifer Jiyoung Huseby University of Michigan, Divya Ramesh University of Michigan, Alice Liu University of Michigan, Sam Mikell University of Michigan, Nina Cahill University of Michigan, Ben Green University of Michigan, Nikola Banovic University of Michigan
File Attached
15:05 - 16:20
Contributed talksLAFI at LAFI
Chair(s): Christine Tasson Sorbonne Université — LIP6
15:05
18m
Talk
Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic LanguagesRemote
LAFI
Alexander K. Lew Massachusetts Institute of Technology, USA, Mathieu Huot Oxford University, Vikash K. Mansinghka MIT
File Attached
15:23
18m
Talk
A Language and Smoothed Semantics for Convergent Stochastic Gradient DescentRemote
LAFI
Dominik Wagner University of Oxford, C.-H. Luke Ong University of Oxford
File Attached
15:42
18m
Talk
Nonparametric Involutive Markov Chain Monte CarloRemote
LAFI
Carol Mak University of Oxford, Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford
File Attached
16:01
18m
Talk
Rigorous Approximation of Posterior Inference for Probabilistic ProgramsRemote
LAFI
Fabian Zaiser University of Oxford, Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford
File Attached
15:05 - 16:35
SRC PostersStudent Research Competition at SRC

Click here for the video posters.

15:05 - 16:35
Satisfiability Modulo TheoriesVMCAI at Salon I
Chair(s): Natarajan Shankar SRI International, USA
15:05
30m
Paper
Generalized Arrays for Stainless FramesRemote
VMCAI
Georg Stefan Schmid EPFL, Switzerland, Viktor Kunčak EPFL, Switzerland
15:35
30m
Paper
NP Satisfiability for Arrays as PowersInPerson
VMCAI
Rodrigo Raya EPFL, Viktor Kunčak EPFL, Switzerland
16:05
30m
Paper
Bit-Precise Reasoning via Int-BlastingRemote
VMCAI
Yoni Zohar Bar Ilan University, Ahmed Irfan Stanford University, Makai Mann Stanford University, Aina Niemetz Stanford University, Andres Nötzli Stanford University, USA, Mathias Preiner Stanford University, Andrew Reynolds University of Iowa, Clark Barrett Stanford University, Cesare Tinelli University of Iowa
15:05 - 15:25
Long talks #4ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
15:05
20m
Talk
Stipula: a domain specific language for legal contractsRemote
ProLaLa
Silvia Crafa University of Padova, Cosimo Laneve University of Bologna, Giovanni Sartor University of Bologna
Pre-print File Attached
15:25 - 16:10
Industry keynoteProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
15:25
45m
Industry talk
Industry keynote -- What does a toolchain for legislation eventually become?Remote
ProLaLa
Davin Fifield Oracle, Surend Dayal Australian National University, Don Syme Microsoft
Link to publication
16:10 - 16:30
Long talks #5ProLaLa at Salon III
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:10
20m
Talk
Ergo - a programming language for Smart Legal ContractsRemote
ProLaLa
Niall Roche Mishcon de Reya,University College London,Accord Project, Jerome Simeon Clause, Walter Hernandez Mishcon de Reya,Accord Project, Eason Chen Accord Project, Dan Selman Docusign,Accord Project
Pre-print File Attached
16:40 - 17:30
KeynoteLAFI at LAFI
Chair(s): Ohad Kammar University of Edinburgh, Christine Tasson Sorbonne Université — LIP6
16:40
50m
Keynote
Program Analysis of Probabilistic ProgramsRemote
LAFI
Maria I. Gorinova The University of Edinburgh
File Attached
16:40 - 17:40
Long talks #6ProLaLa at Salon III
Chair(s): Shrutarshi Basu Harvard University
16:40
20m
Talk
A General Library of Legal ComponentsRemote
ProLaLa
Chris Bailey University of Illinois College of Law
Link to publication
17:00
20m
Talk
Overview of the CCLAW L4 projectRemote
ProLaLa
Avishkar Mahajan Singapore Management University, Martin Strecker Singapore Management University, Meng Weng Wong Singapore Management University
17:20
20m
Talk
Turning Catala into a Proof Platform for the LawRemote
ProLaLa
Alain Delaët INRIA, ENS Lyon, Denis Merigoux INRIA, Aymeric Fromherz Inria
Pre-print

Mon 17 Jan

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

08:50 - 09:00
Welcome from the chairsCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
08:50
10m
Talk
Chairs' report
CPP

File Attached
09:00 - 10:00
Invited talkPADL at Directors
Chair(s): James Cheney University of Edinburgh; Alan Turing Institute

Remote session chair

09:00
60m
Keynote
People, Ideas, and the Path AheadIn-Person
PADL
Marcello Balduccini Saint Joseph's University, USA
09:00 - 10:00
Tutorials 1TutorialFest at Independence
Chair(s): Ning Luo
09:00
60m
Tutorial
Program Analysis via Graph Reachability: Past, Present, and Future [Part A]Remote
TutorialFest
Thomas Reps University of Wisconsin--Madison
09:00 - 10:00
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
09:00
60m
Keynote
Back to the Future: A Fresh Look at Linear Temporal LogicRemote
VMCAI
09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
09:00
60m
Talk
Coq’s vibrant ecosystem for verification engineeringInPerson
CPP
I: Andrew Appel Princeton
Link to publication
10:00 - 10:15
Welcome & AnnouncementPEPM at PEPM
10:00
15m
Day opening
Welcome & AnnouncementRemote
PEPM
Zena M. Ariola University of Oregon, Youyou Cong Tokyo Institute of Technology, Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
10:15 - 11:15
Keynote 1PEPM at PEPM
Chair(s): Sam Lindley The University of Edinburgh, UK
10:15
60m
Keynote
Why are partial evaluation and supercompilation still not widely used in practice? Reflections in light of Russian work on metacomputation.Remote
PEPM
Andrei Klimov Keldysh Institute of Applied Mathematics of Russian Academy of Sciences
File Attached
10:20 - 12:00
Languages, Methods and ToolsPADL at Directors
Chair(s): Esra Erdem Sabanci University, Turkey

Remote session chair

10:20
25m
Talk
Smart Devices and Large Scale Reasoning via ASP: Tools and ApplicationsRemote
PADL
Kristian Reale Department of Mathematics and Computer Science University of Calabria - DLVSystem S.r.l., Francesco Calimeri University of Calabria, Nicola Leone University of Calabria, Italy, Francesco Ricca University of Calabria, Italy
10:45
25m
Talk
Timed Concurrent Language for Argumentation: an Interleaving ApproachRemote
PADL
Stefano Bistarelli University of Perugia, Maria Chiara Meo University “G. d’Annunzio” of Chieti-Pescara, Carlo Taticchi University of Perugia
11:10
25m
Talk
Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set ProgrammingRemote
PADL
Joaquín Arias Universidad Rey Juan Carlos, Manuel Carro IMDEA Software Institute and T.U. of Madrid (UPM), Gopal Gupta The University of Texas at Dallas
DOI Pre-print File Attached
11:35
25m
Talk
Implementing Stable-Unstable Semantics with ASPTOOLS and ClingoRemote
PADL
Tomi Janhunen Tampere University
10:20 - 11:50
Tutorials 2TutorialFest at Independence
Chair(s): Ning Luo
10:20
90m
Tutorial
Program Analysis via Graph Reachability: Past, Present, and Future [Part B]InPerson
TutorialFest
Qirun Zhang Georgia Institute of Technology
10:20 - 11:50
Model CheckingVMCAI at Salon I
Chair(s): Arie Gurfinkel University of Waterloo
10:20
30m
Paper
Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote
VMCAI
Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University
10:50
30m
Paper
Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote
VMCAI
Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA)
Link to publication DOI Pre-print Media Attached File Attached
11:20
30m
Paper
Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson
VMCAI
Landon Taylor Utah State University, Zhen Zhang Utah State University
11:35 - 12:35
Contributed Talks 1PEPM at PEPM
Chair(s): Antonina Nepeivoda Program Systems Institute of RAS, Russia
11:35
30m
Talk
Partially Evaluating Symbolic Interpreters for AllRemote
PEPM
Shangyin Tan Purdue University, Guannan Wei Purdue University, Tiark Rompf Purdue University
File Attached
12:05
30m
Talk
Parallel Algebraic Effect HandlersRemote
PEPM
Ningning Xie University of Cambridge, Daniel D. Johnson Google Research, Dougal Maclaurin Google Research, Adam Paszke Google Research
File Attached
12:55 - 13:55
Keynote 2PEPM at PEPM
Chair(s): William J. Bowman University of British Columbia
12:55
60m
Keynote
From meta frameworks and transformations to distributed computing and moreRemote
PEPM
Y. Annie Liu Stony Brook University
13:30 - 14:45
Answer Set ProgrammingPADL at Directors
Chair(s): Martin Gebser University of Klagenfurt, Austria

Remote session chair

13:30
25m
Talk
Modelling the Outlier Detection Problem in QASPRemote
PADL
Pierpaolo Bellusci University of Calabria, Giuseppe Mazzotta University of Calabria, Fracesco Ricca University of Calabria
13:55
25m
Talk
Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path FindingRemote
PADL
Nima Tajelipirbazari TED University, Çağrı Uluç Yıldırımoğlu Sabanci University, Orkunt Sabuncu TED University, Ali Can Arıcı Ekol Logistics, İdil Helin Özen Ekol Logistics, Volkan Patoğlu Sabanci University, Esra Erdem Sabanci University, Turkey
14:20
25m
Talk
Determining Action Reversibility in STRIPS Using Answer Set Programming with QuantifiersRemote
PADL
Wolfgang Faber University of Klagenfurt, Michael Morak University of Klagenfurt, Lukas Chrpa Czech Technical University in Prague
13:30 - 14:30
Tutorials 3TutorialFest at Independence
Chair(s): Yuyang Sang Yale University
13:30
60m
Tutorial
Formal Methods and Deep Learning [Part A]Remote
TutorialFest
Matthew Mirman ETH Zurich
13:30 - 14:30
Formal Methods in Machine LearningVMCAI at Salon I
Chair(s): Rupak Majumdar MPI-SWS
13:30
30m
Paper
Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned SystemsRemote
VMCAI
David Bayani Carnegie Mellon University's School of Computer Science, Stefan Mitsch Carnegie Mellon University, USA
14:00
30m
Paper
Bisimulations for Neural Network ReductionInPerson
VMCAI
Pavithra Prabhakar Kansas State University
13:30 - 15:10
Semantics and Program VerificationCPP at Salon III
Chair(s): Benjamin Delaware Purdue University
13:30
25m
Talk
A Compositional Proof Framework for FRETish RequirementsRemote
CPP
Esther Conrad NASA LaRC, Laura Titolo NIA/NASA LaRC, Dimitra Giannakopoulou NASA Ames Research Center, Thomas Pressburger NASA ARC, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
13:55
25m
Talk
Verbatim++: Verified, Optimized, and Semantically Rich Lexing with DerivativesRemote
CPP
Derek Egolf Northeastern University, Sam Lasser Tufts University, Kathleen Fisher Tufts University
Link to publication Media Attached
14:20
25m
Talk
Formally Verified Superblock SchedulingInPerson
CPP
Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Leo Gourdin Université Grenoble-Alpes, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux CNRS/VERIMAG, Justus Fasse Université Grenoble-Alpes; KU Leuven, Nicolas Nardino École normale supérieure de Lyon
DOI Pre-print
14:45
25m
Talk
Overcoming Restraint: Composing Verification of Foreign Functions with CogentRemote
CPP
Louis Cheung University of Melbourne, Liam O'Connor University of Edinburgh, Christine Rizkallah University of Melbourne
DOI Pre-print Media Attached
14:15 - 15:15
Keynote 3PEPM at PEPM
Chair(s): Keiko Nakata SAP Innovation Center Potsdam
14:15
60m
Keynote
Modal Logics and Types: Looking Back and Looking ForwardRemote
PEPM
Frank Pfenning Carnegie Mellon University, USA
15:00 - 16:30
Tutorials 4TutorialFest at Independence
Chair(s): Yuyang Sang Yale University
15:00
90m
Tutorial
Formal Methods and Deep Learning [Part B]InPerson
TutorialFest
Gagandeep Singh University of Illinois at Urbana-Champaign; VMware
15:05 - 16:35
Program VerificationVMCAI at Salon I
Chair(s): Elizabeth Polgreen University of Edinburgh
15:05
30m
Paper
High Assurance Software for Financial Regulation and Business PlatformsRemote
VMCAI
Stephen Goldbaum Morgan Stanley, Attila Mihaly Morgan Stanley, Tosha Ellison Fintech Open Source Foundation, Earl Barr UCL, Mark Marron Microsoft Research
15:35
30m
Paper
Loop Verification with Invariants and ContractsRemote
VMCAI
Gidon Ernst Ludwig Maximilian University of Munich
Pre-print
16:05
30m
Paper
Making PROGRESS in Property Directed ReachabilityRemote
VMCAI
Tobias Seufert University of Freiburg, Christoph Scholl University of Freiburg, Arun Chandrasekharan OneSpin Solutions, Munich, Sven Reimer OneSpin Solutions, Munich, Tobias Welp OneSpin Solutions, Munich
15:30 - 17:10
Security and Distributed SystemsCPP at Salon III
Chair(s): Alwyn Goodloe NASA Langley Research Center
15:30
25m
Talk
Reflection, Rewinding, and Coin-Toss in EasyCryptRemote
CPP
Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu
Pre-print Media Attached
15:55
25m
Talk
A verified algebraic representation of Cairo program executionRemote
CPP
Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd.
Pre-print
16:20
25m
Talk
Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson
CPP
William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University
Pre-print
16:45
25m
Talk
Forward build systems, formallyInPerson
CPP
Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University
Link to publication
17:30 - 18:30
Invited TalkCPP at Salon III
Chair(s): Andrei Popescu University of Sheffield
17:30
60m
Talk
The seL4 verification: the art and craft of proof and the reality of commercial supportRemote
CPP
I: June Andronick Proofcraft, UNSW and seL4 Foundation
Media Attached

Tue 18 Jan

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

04:00 - 05:00
Keynote 4PEPM at PEPM
Chair(s): Youyou Cong Tokyo Institute of Technology
04:00
60m
Keynote
On Type-Based Techniques for Program ManipulationRemote
PEPM
Naoki Kobayashi University of Tokyo, Japan
05:20 - 06:35
Contributed Talks 2PEPM at PEPM
Chair(s): Jonathan Immanuel Brachthäuser University of Tübingen
05:20
45m
Talk
Two-level Just-in-Time Compilation with One Interpreter and One EngineRemote
PEPM
Yusuke Izawa Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology, Carl Friedrich Bolz-Tereick Heinrich-Heine-Universität Düsseldorf
Pre-print Media Attached File Attached
06:05
30m
Talk
let (rec) insertion without Effects, Lights or MagicRemote
PEPM
Oleg Kiselyov Tohoku University, Japan, Jeremy Yallop University of Cambridge
Pre-print
06:55 - 07:55
Keynote 5PEPM at PEPM
Chair(s): Julia Lawall Inria
06:55
60m
Keynote
A partial history of partial evaluationRemote
PEPM
Peter Sestoft IT University of Copenhagen
08:15 - 09:15
Contributed Talks 3PEPM at PEPM
Chair(s): Youyou Cong Tokyo Institute of Technology
08:15
30m
Talk
Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent TypesRemote
PEPM
Christopher Brown University of St. Andrews, UK, Adam D. Barwell Imperial College London, UK, Yoann Marquer INRIA, Rennes, France, Olivier Zendra INRIA, Rennes, France, Tania Richmond INRIA, Rennes, France then DGA - Maîtrise de l’Information, Chen Gu Hefei University of Technology, China
Link to publication
08:45
30m
Talk
Dependent tagless finalRemote
PEPM
Nicolas Biri Luxembourg Institute of Science and Technology
Link to publication
09:00 - 10:00
Invited talkPADL at Directors
Chair(s): Antonio Brogi Università di Pisa, Simona Perri University of Calabria, Italy

Remote session chair

09:00
60m
Keynote
Declarative Programming and EducationRemote
PADL
Shriram Krishnamurthi Brown University, United States
09:00 - 10:00
Morning 1PLMW at Independence
Chair(s): Robbert Krebbers Radboud University Nijmegen
09:00
20m
Day opening
Welcome by POPL 2022 Program ChairRemote
PLMW
09:25
35m
Talk
Automatically Synthesising Programs that We Can TrustRemote
PLMW
Ilya Sergey National University of Singapore
09:00 - 10:00
SynthesisVMCAI at Salon I
Chair(s): Viktor Kunčak EPFL, Switzerland
09:00
30m
Paper
Gradient-Descent for Randomized Controllers under Partial ObservabilityInPerson
VMCAI
Jip Spel RWTH Aachen University, Linus Heck RWTH Aachen University, Sebastian Junges University of California, Berkeley, Joshua Moerman Open University of the Netherlands, Joost-Pieter Katoen RWTH Aachen University
09:30
30m
Paper
Satisfiability and Synthesis Modulo OraclesRemote
VMCAI
Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley
09:00 - 10:00
Invited TalkCPP at Salon III
Chair(s): Laura Titolo NIA/NASA LaRC
09:00
60m
Talk
Structural Embeddings RevisitedRemote
CPP
10:20 - 12:00
Declarative SolutionsPADL at Directors
Chair(s): Francesco Calimeri University of Calabria

Remote session chair

10:20
25m
Talk
Green Application Placement in the Cloud-IoT ContinuumRemote
PADL
Stefano Forti University of Pisa, Antonio Brogi Università di Pisa
10:45
25m
Talk
Decomposition-based job-shop scheduling with constrained clusteringRemote
PADL
Mohammed M. S. El-Kholany University of Klagenfurt, Martin Gebser University of Klagenfurt, Austria, Konstantin Schekotihin Alpen-Adria Universit�t Klagenfurt
11:10
25m
Talk
Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)Remote
PADL
Sarat Chandra Varanasi The University of Texas at Dallas, Joaquín Arias Universidad Rey Juan Carlos, Elmer Salazar The University of Texas at Dallas, Fang Li The University of Texas at Dallas, Kinjal Basu The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas
11:35
25m
Talk
Parallel Declarative Solutions of Sequencing Problems using Multi-valued Decision Diagrams and GPUsRemote
PADL
Fabio Tardivo New Mexico State University, Enrico Pontelli
10:20 - 11:10
Morning 2PLMW at Independence
Chair(s): Paul Downen University of Massachusetts Lowell
10:20
50m
Talk
You and Your EnvironmentIn-person
PLMW
Talia Ringer University of Illinois at Urbana-Champaign
10:20 - 11:50
Probabilistic SystemsVMCAI at Salon I
Chair(s): Pavithra Prabhakar Kansas State University
10:20
30m
Paper
Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson
VMCAI
Tobias Winkler RWTH Aachen University, Johannes Lehmann RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
10:50
30m
Paper
STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote
VMCAI
Riley Roberts Utah State University, Thakur Neupane The MathWorks, Inc., Lukas Buecherl University of Colorado, Boulder, Chris Myers University of Colorado, Boulder, Zhen Zhang Utah State University
11:20
30m
Paper
EPMC Gets Knowledge in Multi-Agent SystemsRemote
VMCAI
Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
10:20 - 12:00
Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III
Chair(s): Steve Zdancewic University of Pennsylvania
10:20
25m
Talk
CertiStr: A Certified String SolverDistinguished Paper AwardRemote
CPP
Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern
DOI Pre-print Media Attached
10:45
25m
Talk
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote
CPP
Michael Färber Universität Innsbruck, Austria
DOI Pre-print Media Attached File Attached
11:10
25m
Talk
An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote
CPP
Pre-print Media Attached
11:35
25m
Talk
A Drag-and-Drop Proof TacticRemote
CPP
Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique
DOI Pre-print Media Attached
11:10 - 12:00
Morning 3 (live only, no recording)PLMW at Independence
Chair(s): Stephanie Balzer Carnegie Mellon University
11:10
50m
Panel
Panel (live only, no recording)Hybrid
PLMW
François Pottier Inria, Azadeh Farzan University of Toronto, Henry DeYoung CMU, Wen Kokke University of Edinburgh, Stephanie Weirich University of Pennsylvania, Ralf Jung MPI-SWS
13:30 - 14:45
Functional and Logic ProgrammingPADL at Directors
Chair(s): Alan Jeffrey Roblox
13:30
25m
Talk
Graph-based Interpretation of Normal Logic ProgramsRemote
PADL
Fang Li The University of Texas at Dallas, Elmer Salazar The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas
13:55
25m
Talk
Functional Programming on Top of SQL EnginesRemote
PADL
Tobias Burghardt University of Tübingen, Denis Hirn University of Tübingen, Torsten Grust University of Tübingen
14:20
25m
Talk
CircuitFlow: : A Domain Specific Language for Dataflow ProgrammingIn-Person
PADL
Riley Evans University of Bristol, Samantha Frohlich University of Bristol, Meng Wang University of Bristol
13:30 - 14:45
Afternoon 1PLMW at Independence
Chair(s): Stephanie Balzer Carnegie Mellon University
13:30
35m
Talk
Implementing Languages for Fun and ProfitRemote
PLMW
14:10
35m
Talk
Writing Valuable PapersRemote
PLMW
Liam O'Connor University of Edinburgh
13:30 - 14:30
Invited TalkVMCAI at Salon I
Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security
13:30
60m
Keynote
Simplifying Concurrent Programming via Synchronization SynthesisRemote
VMCAI
Isil Dillig University of Texas at Austin
15:05 - 16:20
Afternoon 2PLMW at Independence
Chair(s): Paul Downen University of Massachusetts Lowell
15:05
35m
Talk
Proving and ProgrammingRemote
PLMW
Zena M. Ariola University of Oregon
15:45
35m
Talk
Finding a research topic (or being found by a research topic?)Remote
PLMW
Alexandra Silva Cornell University
15:05 - 16:35
SRC PresentationsStudent Research Competition at SRC

Click here for the video posters.

15:05
15m
Talk
Towards a Syntactic Model of Sized Dependent Types
Student Research Competition
Jonathan Chan University of British Columbia (UBC)
Media Attached
15:20
15m
Talk
Dependent-Type-Preserving Memory Allocation
Student Research Competition
Paulette Koronkevich University of British Columbia
15:35
15m
Talk
Linearity, Uniqueness, Ownership: An Entente Cordiale
Student Research Competition
Daniel Marshall University of Kent, UK
Media Attached
15:50
15m
Talk
CapableWasm: Bringing Better Interop Down to WebAssembly
Student Research Competition
16:05
15m
Talk
Filling a Niche: Using Spare Bits to Optimize Data Representations
Student Research Competition
16:20
15m
Talk
A Realizability Model for Interoperability Between Languages with Garbage-Collected and Manually Managed Memory
Student Research Competition
Noble Mushtak Northeastern University
15:05 - 16:05
Static Analysis and Hybrid SystemsVMCAI at Salon I
Chair(s): Yoni Zohar Bar Ilan University
15:05
30m
Paper
Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson
VMCAI
Jan Onderka Czech Technical University in Prague, Stefan Ratschan The Czech Academy of Sciences
15:35
30m
Paper
Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid AutomataRemote
VMCAI
Yuming Wu Nanjing University, Lei Bu Nanjing University, Jiawan Wang Nanjing University, Xinyue Ren Nanjing University, Wen Xiong Nanjing University, Xuandong Li Nanjing University
15:30 - 16:10
Chairs' Report and Business MeetingCPP at Salon III
Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania
15:30
40m
Talk
Chairs' Report
CPP

File Attached
16:30 - 18:10
Category Theory, HoTT, Number TheoryCPP at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
16:30
25m
Talk
Implementing a category-theoretic framework for typed abstract syntaxRemote
CPP
Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University
DOI Pre-print Media Attached
16:55
25m
Talk
(Deep) Induction Rules for GADTsRemote
CPP
Patricia Johann Appalachian State University, Enrico Ghiorzi Italian Institute of Technology
Pre-print Media Attached
17:20
25m
Talk
On homotopy of walks and spherical maps in homotopy type theoryRemote
CPP
Jonathan Prieto-Cubides University of Bergen
Pre-print Media Attached
17:45
25m
Talk
Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote
CPP
Hing Lun Chan Australian National University
DOI Pre-print Media Attached File Attached

Wed 19 Jan

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

08:00 - 09:00
BreakfastPOPL at Salon II
08:50 - 09:00
WelcomePOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania, Hongseok Yang KAIST
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
09:00
60m
Keynote
Principles of Programming Language TranslatorsRemoteInvited Talk
POPL
Alfred V. Aho Columbia University
10:00 - 10:20
SIGPLAN CARESDiversity, Equity and Inclusion at Salon II
Chair(s): Stephanie Weirich University of Pennsylvania

Only in person

10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Automated VerificationPOPL at Salon I
Chair(s): Roberto Giacobazzi University of Verona
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University
DOI Media Attached
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo
DOI Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
POPL
Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Media Attached
12:00 - 13:30
Women@POPL LunchDiversity, Equity and Inclusion at Independence

Only in person

12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
Program AnalysisPOPL at Salon I
Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign; VMware
13:30
25m
Research paper
Property-Directed Reachability as Abstract Interpretation in the Monotone TheoryRemote
POPL
Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox Certora
DOI Media Attached
13:55
25m
Research paper
Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program AnalysisInPerson
POPL
Marco Campion University of Verona, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Verona
DOI Media Attached
14:20
25m
Research paper
Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented ProgramsInPerson
POPL
Minseok Jeon Korea University, Hakjoo Oh Korea University
DOI Media Attached
13:30 - 14:45
Weak Memory ModelsPOPL at Salon III
Chair(s): Mae Milano University of California, Berkeley
13:30
25m
Research paper
The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson
POPL
Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University
DOI Media Attached
13:55
25m
Research paper
Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal StoresRemote
POPL
Azalea Raad Imperial College London, Luc Maranget Inria, Viktor Vafeiadis MPI-SWS
DOI Media Attached
14:20
25m
Research paper
Truly Stateless, Optimal Dynamic Partial Order ReductionRemote
POPL
Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS
DOI Media Attached
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
Algorithmic Verification 1POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology
15:05
25m
Research paper
Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote
POPL
Yuanbo Li Georgia Institute of Technology, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
DOI Media Attached
15:30
25m
Research paper
The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemote
POPL
Adam Husted Kjelstrøm Aarhus University, Andreas Pavlogiannis Aarhus University
DOI Media Attached
15:55
25m
Research paper
Subcubic Certificates for CFL ReachabilityRemote
POPL
Dmitry Chistikov University of Warwick, Rupak Majumdar MPI-SWS, Philipp Schepper CISPA
DOI Media Attached
15:05 - 16:20
Concurrency and ParallelismPOPL at Salon III
Chair(s): Andrew C. Myers Cornell University
15:05
25m
Research paper
Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote
POPL
Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
15:30
25m
Research paper
Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote
POPL
Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen
DOI Media Attached
15:55
25m
Research paper
Static Prediction of Parallel Computation GraphsInPerson
POPL
Stefan K. Muller Illinois Institute of Technology
DOI Media Attached
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 17:30
Algorithmic Verification 2POPL at Salon I
Chair(s): Qirun Zhang Georgia Institute of Technology
16:40
25m
Research paper
Context-Bounded Verification of Thread PoolsRemote
POPL
DOI Media Attached
17:05
25m
Research paper
What’s Decidable about Linear Loops?InPerson
POPL
Toghrul Karimov MPI-SWS, Engel Lefaucheux MPI-SWS, Joël Ouaknine MPI-SWS, David Purser MPI-SWS, Anton Varonka MPI-SWS, Markus A. Whiteland MPI-SWS, James Worrell University of Oxford
DOI Pre-print Media Attached
16:40 - 17:30
Reasoning about Probabilistic Programs and AlgorithmsPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
16:40
25m
Research paper
A Separation Logic for Negative DependenceRemote
POPL
Jialu Bao Cornell University, Marco Gaboardi Boston University, Justin Hsu Cornell University, Joseph Tassarotti Boston College
DOI Media Attached
17:05
25m
Research paper
Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote
POPL
Yizhou Zhang University of Waterloo, Nada Amin Harvard University
DOI Media Attached
18:00 - 20:00
ReceptionPOPL at Salon II

Thu 20 Jan

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

08:00 - 09:00
Junior Faculty Mentoring BreakfastDiversity, Equity and Inclusion at Independence
Chair(s): Michael Hicks University of Maryland at College Park

Only in person

08:00 - 09:00
BreakfastPOPL at Salon II
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Michael Hicks University of Maryland at College Park
09:00
60m
Keynote
Better Learning through Programming LanguagesInvited TalkInPerson
POPL
Armando Solar-Lezama Massachusetts Institute of Technology
10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Foundation and Verification of Machine-Learning SystemsPOPL at Salon I
Chair(s): Gilbert Louis Bernstein University of California at Berkeley
10:20
25m
Research paper
A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson
POPL
Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI Media Attached
10:45
25m
Research paper
Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote
POPL
Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore
DOI Media Attached
11:10
25m
Research paper
Interval Universal Approximation for Neural NetworksInPerson
POPL
Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin
DOI Media Attached
11:35
25m
Research paper
PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson
POPL
Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
DOI Media Attached
10:20 - 12:00
Quantum ComputingPOPL at Salon III
Chair(s): Michael Hicks University of Maryland at College Park
10:20
25m
Research paper
Quantum Information EffectsRemote
POPL
Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Edinburgh
DOI Media Attached
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI Media Attached
11:10
25m
Research paper
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote
POPL
Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University
DOI Media Attached
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria
DOI Media Attached
12:00 - 13:30
LGBTQ@POPL LunchDiversity, Equity and Inclusion at Independence

Only in person

12:00 - 13:30
LunchPOPL at Salon II
13:30 - 14:45
TypesPOPL at Salon I
Chair(s): Stephanie Weirich University of Pennsylvania
13:30
25m
Research paper
On Type-Cases, Union Elimination, and Occurrence TypingInPerson
POPL
Giuseppe Castagna CNRS; Université de Paris, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay, Matthew Lutze Université de Paris
DOI Media Attached
13:55
25m
Research paper
Oblivious Algebraic Data TypesInPerson
POPL
Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
DOI Media Attached
14:20
25m
Research paper
SolType: Refinement Types for Arithmetic Overflow in SolidityRemote
POPL
Bryan Tan University of California at Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu K. Lahiri Microsoft Research, Isil Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
DOI Media Attached
13:30 - 14:45
Dynamic AnalysisPOPL at Salon III
Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology
13:30
25m
Research paper
A Formal Foundation for Symbolic Evaluation with MergingRemote
POPL
Sorawee Porncharoenwase University of Washington, Luke Nelson University of Washington, Xi Wang University of Washington, Emina Torlak University of Washington
DOI Media Attached
13:55
25m
Research paper
Logarithm and Program TestingInPerson
POPL
Kuen-Bang Hou (Favonia) University of Minnesota, Zhuyang Wang University of Minnesota
DOI Media Attached
14:20
25m
Research paper
Profile Inference RevisitedRemote
POPL
Wenlei He Facebook, Julián Mestre Facebook; University of Sydney, Sergey Pupyrev , Lei Wang Facebook, Hongtao Yu Facebook
DOI Media Attached
14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
SystemsPOPL at Salon I
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Research paper
Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson
POPL
Matthew Kolosick University of California at San Diego, Shravan Ravi Narayan University of California at San Diego, Evan Johnson University of California at San Diego, Conrad Watt University of Cambridge, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego
DOI Media Attached
15:30
25m
Research paper
Relational E-matchingRemote
POPL
Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington
DOI Media Attached
15:55
25m
Research paper
Linked Visualisations via Galois DependenciesRemote
POPL
Roly Perera Alan Turing Institute, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol
DOI Media Attached
15:05 - 16:20
MetaprogrammingPOPL at Salon III
Chair(s): Stephanie Weirich University of Pennsylvania
15:05
25m
Research paper
Staging with Class: A Specification for Typed Template HaskellInPerson
POPL
Ningning Xie University of Cambridge, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol
DOI Media Attached
15:30
25m
Research paper
Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote
POPL
Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University
DOI Media Attached
15:55
25m
Research paper
Type-Level Programming with Match TypesRemote
POPL
DOI Media Attached
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 18:00
POPL Business Meeting and SIGPLAN AwardsPOPL at Salon I
Chair(s): Rajeev Alur University of Pennsylvania
16:40
10m
Meeting
General Chair ReportInPerson
POPL
Rajeev Alur University of Pennsylvania
16:50
10m
Meeting
Program Chair ReportRemote
POPL
17:00
10m
Meeting
Virtualization Chair ReportRemote
POPL
Adam Chlipala Massachusetts Institute of Technology
17:10
5m
Meeting
POPL 2023 ReportInPerson
POPL
Andrew C. Myers Cornell University
17:15
3m
Awards
Student Research Competition WinnersRemote
POPL
Azalea Raad Imperial College London
17:18
3m
Awards
POPL'22 Distinguished PapersRemote
POPL
17:21
3m
Awards
SIGPLAN Reynolds Dissertation AwardRemote
POPL
Isil Dillig University of Texas at Austin
17:24
3m
Awards
POPL Most Influential Paper AwardRemote
POPL
Tony Hosking Australian National University
17:27
3m
Awards
SIGPLAN Programming Languages Achievements AwardRemote
POPL
Isil Dillig University of Texas at Austin
17:30
10m
Awards
Remarks by SIGPLAN PL Achievements Award WinnerRemote
POPL

17:40
20m
Meeting
Open Forum for Q&AInPerson
POPL
Rajeev Alur University of Pennsylvania

Fri 21 Jan

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

08:00 - 09:00
Graduating PhDs / Postdocs Mentoring BreakfastDiversity, Equity and Inclusion at Independence
Chair(s): Andrew C. Myers Cornell University

Only in person

08:00 - 09:00
BreakfastPOPL at Salon II
09:00 - 10:00
Invited TalkPOPL at Salon I
Chair(s): Adam Chlipala Massachusetts Institute of Technology
09:00
60m
Keynote
Coalgebra for the working programming languages researcherRemoteInvited Talk
POPL
Alexandra Silva Cornell University
10:00 - 10:20
BreakPOPL at Salon II
10:20 - 12:00
Distributed or Network ProgramsPOPL at Salon I
Chair(s): J. Garrett Morris The University of Iowa
10:20
25m
Research paper
Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson
POPL
Andrew K. Hirsch MPI-SWS, Deepak Garg MPI-SWS
DOI Media Attached
10:45
25m
Research paper
Fair Termination of Binary SessionsRemote
POPL
Luca Ciccone University of Turin, Luca Padovani University of Turin
DOI Media Attached
11:10
25m
Research paper
Safe, Modular Packet Pipeline ProgrammingRemote
POPL
Devon Loehr Princeton University, David Walker Princeton University
DOI Media Attached
11:35
25m
Research paper
Dependently-Typed Data Plane ProgrammingRemote
POPL
Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
DOI Media Attached
10:20 - 12:00
Semantics 1POPL at Salon III
Chair(s): Alan Jeffrey Roblox
10:20
25m
Research paper
From Enhanced Coinduction towards Enhanced InductionRemote
POPL
Davide Sangiorgi University of Bologna; Inria
DOI Media Attached
10:45
25m
Research paper
A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson
POPL
Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France
DOI Media Attached
11:10
25m
Research paper
Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote
POPL
Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford
DOI Media Attached
11:35
25m
Research paper
Layered and Object-Based Game SemanticsInPerson
POPL
Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS; Université de Paris, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS
DOI Media Attached
12:00 - 13:30
LunchPOPL at Salon II
12:30 - 13:30
ShutdownPLDiversity, Equity and Inclusion at Salon I
Chair(s): David Justo Microsoft Azure
12:30
60m
Talk
Designing and Developing for the Black ExperienceRemote
Diversity, Equity and Inclusion
Brittany Johnson George Mason University
13:30 - 14:45
TOPLAS SessionPOPL at Salon I
Chair(s): Andrew C. Myers Cornell University
13:30
25m
Talk
Armed cats: formal concurrency modelling at ArmRemote
POPL
Jade Alglave University College London, Will Deacon ARM Ltd., Richard Grisenthwaite , Antoine Hacquard EPITA, LRDE, Luc Maranget Inria
13:55
25m
Talk
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Remote
POPL
Emanuele D'Osualdo MPI-SWS, Julian Sutherland Imperial College London, Azadeh Farzan University of Toronto, Philippa Gardner Imperial College London
DOI
14:20
25m
Talk
Gradualizing the Calculus of Inductive ConstructionsRemote
POPL
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile
13:30 - 14:45
Semantics 2POPL at Salon III
Chair(s): Marco Gaboardi Boston University
13:30
25m
Research paper
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson
POPL
Vikraman Choudhury Indiana University; University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University
Link to publication DOI Media Attached
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
14:45 - 15:05
SIGPLAN CARESDiversity, Equity and Inclusion at Salon II
Chair(s): Stephanie Weirich University of Pennsylvania

Only in person

14:45 - 15:05
BreakPOPL at Salon II
15:05 - 16:20
Verification 1POPL at Salon I
Chair(s): Lennart Beringer Princeton University
15:05
25m
Research paper
Certifying Derivation of State Machines from CoroutinesInPerson
POPL
Mirai Ikebuchi National Institute of Informatics, Andres Erbsen Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
15:30
25m
Research paper
VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote
POPL
Rodolphe Lepigre MPI-SWS, Michael Sammler MPI-SWS, Kayvan Memarian University of Cambridge, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Peter Sewell University of Cambridge
DOI Media Attached
15:55
25m
Research paper
Verified Compilation of C Programs with a Nominal Memory ModelRemote
POPL
Yuting Wang Shanghai Jiao Tong University, Ling Zhang Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University
DOI Media Attached
15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota
15:05
25m
Research paper
A Cost-Aware Logical FrameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University
DOI Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore University of Cambridge, Dmitrij Szamozvancev University of Cambridge
DOI Media Attached
15:55
25m
Research paper
Observational Equality: Now for GoodDistinguished PaperRemote
POPL
DOI Media Attached
16:20 - 16:40
BreakPOPL at Salon II
16:40 - 17:30
Verification 2POPL at Salon I
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:40
25m
Research paper
Verified Tensor-Program Optimization Via High-Level Scheduling RewritesRemote
POPL
Amanda Liu Massachusetts Institute of Technology, Gilbert Louis Bernstein University of California at Berkeley, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology
DOI Media Attached
17:05
25m
Research paper
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote
POPL
Jay P. Lim Rutgers University, Santosh Nagarakatte Rutgers University
DOI Media Attached
16:40 - 17:30
SynthesisPOPL at Salon III
Chair(s): Paul Downen University of Massachusetts Lowell
16:40
25m
Research paper
Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson
POPL
Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
DOI Media Attached
17:05
25m
Research paper
Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote
POPL
Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Isil Dillig University of Texas at Austin
DOI Media Attached

Sat 22 Jan

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

09:00 - 10:00
Keynote IPriSC at Independence
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
09:00
60m
Keynote
BPF and Spectre: Mitigating transient execution attacksRemote
PriSC
Piotr Krysiuk Symantec, Threat Hunter Team, Benedict Schlüter Ruhr University Bochum, Daniel Borkmann Isovalent
File Attached
09:00 - 10:00
Invited Talk ICoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
09:00
60m
Keynote
Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote
CoqPL
09:00 - 10:00
Session 1WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
09:00
15m
Talk
CN: A Refinement Type System for CRemote
WITS
Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
09:15
45m
Other
Type-aware equational rewriting (discussion)In-Person
WITS
09:15
45m
Other
Multi case trees: confluence and coverage (discussion)In-Person
WITS
Tesla Zhang The Pennsylvania State University
09:15
45m
Other
Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote
WITS
Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
File Attached
09:15
45m
Other
The Expression Problem and Theorem Proving (discussion)Remote
WITS
Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania
10:20 - 11:35
Attacks and defensesPriSC at Independence
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
10:20
25m
Talk
Type-directed Program Transformation for Constant-Time EnforcementRemote
PriSC
File Attached
10:45
25m
Talk
Towards Understanding Spectre-PHT in Memory-Safe LanguagesRemote
PriSC
Zirui Neil Zhao University of Illinois at Urbana-Champaign, Fangfei Liu Intel Corporation, Scott Constable Intel Corporation, Carlos Rozas Intel Corporation
11:10
25m
Talk
Synthesizing Evidence of Emergent ComputationRemote
PriSC
Scott Moore Galois, Inc., Jennifer Paykin Galois, Inc., Olivier Savary Bélanger Galois, Inc.
Media Attached File Attached
10:20 - 12:00
Contributed Talks (Morning)CoqPL at Salon I
Chair(s): Benjamin C. Pierce University of Pennsylvania
10:20
20m
Talk
A Visual Ltac Debugger in CoqIDERemote
CoqPL
S: Jim Fehrle None
File Attached
10:40
20m
Talk
Scrap your boilerplate definitions in 10 lines of Ltac!InPerson
CoqPL
S: Qianchuan Ye Purdue University, Benjamin Delaware Purdue University
File Attached
11:00
20m
Talk
Tealeaves: Categorical structures for syntaxInPerson
CoqPL
S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA
File Attached
11:20
20m
Talk
Towards a Formalization of Nominal Sets in CoqRemote
CoqPL
S: Fabrício S. Paranhos Universidade Federal de Goiás, Daniel Ventura Universidade Federal de Goiás
File Attached
11:40
20m
Talk
A Case for Lightweight Interfaces in CoqInPerson
CoqPL
David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems
File Attached
11:35 - 12:00
Short talksPriSC at Independence
Chair(s): Marco Guarnieri IMDEA Software Institute
13:30 - 14:30
Invited Talk IICoqPL at Salon I
Chair(s): Amin Timany Aarhus University
13:30
60m
Keynote
Verifying Concurrent, Crash-Safe Systems with PerennialRemote
CoqPL
I: Joseph Tassarotti Boston College
13:30 - 14:45
Session 3WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
13:30
15m
Talk
Tries that matchRemote
WITS
Sebastian Graf Karlsruhe Institute of Technology
13:45
15m
Talk
Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote
WITS
Sebastian Ullrich Karlsruhe Institute of Technology
14:00
45m
Other
Benchmarking Binding (discussion)In-Person
WITS
Stephanie Weirich University of Pennsylvania
14:00
45m
Other
Fancy module systems (discussion)Remote
WITS
Jesper Cockx TU Delft
14:30 - 14:50
Contributed Talk (Afternoon)CoqPL at Salon I
Chair(s): Amin Timany Aarhus University
14:30
20m
Talk
A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote
CoqPL
S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University
Pre-print File Attached
15:05 - 16:20
Secure compilation theoryPriSC at Independence
Chair(s): Arthur Azevedo de Amorim Boston University
15:05
25m
Talk
Composing Secure CompilersRemote
PriSC
Matthis Kruse CISPA Helmholtz Center for Information Security, Marco Patrignani CISPA Helmholtz Center for Information Security / Stanford University
File Attached
15:30
25m
Talk
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking SimulationRemote
PriSC
Akram El-Korashy Max Planck Institute for Software Systems (MPI-SWS), Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Jérémy Thibault MPI-SP, Adrien Durier Max Planck Institute for Security and Privacy (MPI-SP), Cătălin Hriţcu MPI-SP, Deepak Garg MPI-SWS
Pre-print Media Attached File Attached
15:55
25m
Talk
The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, AbstractlyRemote
PriSC
Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8
DOI Pre-print File Attached
15:05 - 15:50
Session with the Coq Development TeamCoqPL at Salon I
Chair(s): Amin Timany Aarhus University
15:05
45m
Panel
Session with the Coq Development TeamRemote
CoqPL
S: Matthieu Sozeau Inria, S: Yves Bertot INRIA, S: Hugo Herbelin , S: Emilio Jesús Gallego Arias INRIA, S: Jason Gross MIT CSAIL
15:05 - 16:20
Session 4WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
15:05
15m
Talk
mitten: A Flexible Multimodal Proof AssistantRemote
WITS
Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
15:20
15m
Talk
Understandable and Useful Error Messages for Liquid TypesRemote
WITS
Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
15:35
15m
Talk
Deciding type equivalence with simple grammarsIn-Person
WITS
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
15:50
15m
Talk
Typechecking up to CongruenceIn-Person
WITS
Jad Elkhaleq Ghalayini University of Cambridge
16:05
15m
Talk
À bas l’η — Coq’s troublesome η-conversionRemote
WITS
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes
16:40 - 17:55
Secure systemsPriSC at Independence
Chair(s): Marco Guarnieri IMDEA Software Institute
16:40
25m
Talk
A CompCert backend with symbolic encryptionRemote
PriSC
Paolo Torrini INRIA, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
File Attached
17:05
25m
Talk
Effect-Oblivious EquivalenceRemote
PriSC
Yao Li University of Pennsylvania, Stephanie Weirich University of Pennsylvania
Pre-print File Attached
17:30
25m
Talk
The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating codeRemote
PriSC
Dominic Mulligan Arm Research, Nick Spinale Arm Research
File Attached
16:40 - 17:30
Session 5WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
16:40
15m
Talk
Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person
WITS
Matthew L. Daggitt Heriot-Watt University, Guillaume Allais University of St Andrews
16:55
15m
Talk
Setting the Record Straight with SingletonsRemote
WITS
Reed Mullanix University of Minnesota
17:10
15m
Talk
First-class pattern synonymsIn-Person
WITS
Tesla Zhang The Pennsylvania State University

Thu 27 Jan

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

12:00 - 13:00
Welcome ReceptionVirtual Workshop at Airmeet
12:00
60m
Break
Break at the Airmeet tables ("Lounge")
Virtual Workshop

13:00 - 14:00
Networking: careers at sponsor companies (U.S. time band)Virtual Workshop at Airmeet
13:00
60m
Social Event
Networking: careers at sponsor companies
Virtual Workshop

14:00 - 15:00
Networking: academic job searches and PhD applications (U.S. time band)Virtual Workshop at Airmeet
14:00
60m
Social Event
Networking: academic job searches and PhD applications
Virtual Workshop

15:00 - 16:00
15:00
60m
Panel
Panel 1: proof assistants for PL and math
Virtual Workshop
Kevin Buzzard Imperial College London, Kuen-Bang Hou (Favonia) University of Minnesota, Zhong Shao Yale University, Nicolas Tabareau Inria
16:00 - 18:00
Unstructured Time 1Virtual Workshop at Airmeet
16:00
2h
Break
Unstructured time
Virtual Workshop

18:00 - 19:00
18:00
60m
Keynote
Keynote 1: OpenAI Codex presentation & demo
Virtual Workshop
19:00 - 20:00
Unstructured Time 2Virtual Workshop at Airmeet
19:00
60m
Break
Unstructured time
Virtual Workshop

20:00 - 21:00
Mentoring for graduating PhDs and postdocs (U.S. time band)Virtual Workshop at Airmeet
20:00
60m
Social Event
Mentoring for graduating PhDs and postdocs
Virtual Workshop

21:00 - 03:00
Unstructured Time 3Virtual Workshop at Airmeet
21:00
6h
Break
Unstructured time
Virtual Workshop

Fri 28 Jan

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

03:00 - 04:00
03:00
60m
Panel
PLMW Panel (on Zoom)
Virtual Workshop
Youyou Cong Tokyo Institute of Technology, Andreea Costea School of Computing, National University Of Singapore, Cristina Cifuentes Oracle Labs, Sukyoung Ryu KAIST
04:00 - 05:00
Networking: careers at sponsor companies (Asia time band)Virtual Workshop at Airmeet
04:00
60m
Social Event
Networking: careers at sponsor companies
Virtual Workshop

05:00 - 06:00
Networking: academic job searches and PhD applications (Asia time band)Virtual Workshop at Airmeet
05:00
60m
Social Event
Networking: academic job searches and PhD applications
Virtual Workshop

07:00 - 09:00
Unstructured Time 4Virtual Workshop at Airmeet
07:00
2h
Break
Unstructured time
Virtual Workshop

07:00
2h
Break
Unstructured time
Virtual Workshop

09:00 - 10:00
09:00
60m
Keynote
Keynote 2: on WebAssembly
Virtual Workshop
Andreas Rossberg Dfinity Stiftung
10:00 - 11:00
Unstructured Time 5Virtual Workshop at Airmeet
10:00
60m
Break
Unstructured time
Virtual Workshop

11:00 - 14:00
Unstructured Time 7Virtual Workshop at Airmeet
11:00
3h
Break
Unstructured time
Virtual Workshop

14:00 - 18:00
Unstructured Time 6Virtual Workshop at Airmeet
14:00
4h
Break
Unstructured time
Virtual Workshop

18:00 - 19:00
Mentoring for junior faculty (Asia time band)Virtual Workshop at Airmeet
18:00
60m
Social Event
Mentoring for junior faculty
Virtual Workshop

19:00 - 20:00
19:00
60m
Panel
Panel 2: the future of concurrency and parallelism
Virtual Workshop
Stephanie Balzer Carnegie Mellon University, Jeehoon Kang KAIST, Keshav Pingali The University of Texas at Austin, Ilya Sergey National University of Singapore
20:00 - 21:00
Mentoring for junior faculty (U.S. time band)Virtual Workshop at Airmeet
20:00
60m
Social Event
Mentoring for junior faculty
Virtual Workshop

21:00 - 22:00
Mentoring for graduating PhDs and postdocs (Asia time band)Virtual Workshop at Airmeet
21:00
60m
Social Event
Mentoring for graduating PhDs and postdocs
Virtual Workshop