Write a Blog >>
POPL 2020
Sun 19 - Sat 25 January 2020 New Orleans, Louisiana, United States
POPL 2020 (series) / JW Marriott New Orleans /

Room information: Ile de France III (IDF III)

VenueJW Marriott New Orleans
Room nameIle de France III (IDF III)
Floor3
Room InformationNo extra information available
Program

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

Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00
Morning 1PLMW at Ile de France III (IDF III)
Chair(s): Stephanie Balzer Carnegie Mellon University, USA
09:00
10m
Day opening
Opening
PLMW
Brigitte Pientka McGill University
09:10
50m
Talk
How to Write Papers So People Can Read ThemMentoring Event
PLMW
Derek Dreyer MPI-SWS
File Attached
10:30 - 12:30
Morning 2PLMW at Ile de France III (IDF III)
Chair(s): Robbert Krebbers Delft University of Technology
10:30
40m
Talk
Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event
PLMW
Lindsey Kuper University of California, Santa Cruz
Media Attached
11:10
40m
Talk
Research as a collaborative effortMentoring Event
PLMW
Marco Gaboardi Boston University
Media Attached File Attached
11:50
40m
Talk
Theorem provers are a P.L. researcher's best friendMentoring Event
PLMW
Xavier Leroy Collège de France
Media Attached File Attached
14:00 - 15:05
Afternoon 1PLMW at Ile de France III (IDF III)
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
65m
Talk
PanelMentoring Event
PLMW
William J. Bowman University of British Columbia, Kenny Foner Galois, Andrew K. Hirsch Max Planck Institute for Software Systems, Taro Sekiyama National Institute of Informatics, Juliana Franco Microsoft Research, Cambridge, Hannah Gommerstadt Vassar College
Media Attached
15:35 - 17:45
Afternoon 2PLMW at Ile de France III (IDF III)
Chair(s): Nobuko Yoshida Imperial College London
15:40
60m
Talk
How Can I Academia When My Brain Can't Even? Mental Health in Grad School and BeyondMentoring Event
PLMW
Kenny Foner Galois
Media Attached
16:40
10m
Coffee break
Mini break
PLMW

16:50
45m
Talk
Automated Program Verification using Abductive ReasoningMentoring Event
PLMW
Işıl Dillig University of Texas Austin
Media Attached

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III)
Chair(s): Roopsha Samanta Purdue University
10:30
21m
Talk
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
Research Papers
Yannick Forster Saarland University, Fabian Kunze Saarland University, Marc Roth Saarland University and MMCI and Merton College, Oxford University
Link to publication DOI Pre-print Media Attached
10:51
21m
Talk
Complexity and Information in Invariant Inference
Research Papers
Yotam M. Y. Feldman Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university
Link to publication DOI Media Attached
11:13
21m
Talk
Parameterized Verification under TSO is PSPACE-Complete
Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Rojin Rezvan Sharif University
Link to publication DOI
11:45 - 12:30
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen Lesani University of California, Riverside
11:45
22m
Talk
Program Synthesis by Type-Guided Abstraction Refinement
Research Papers
Zheng Guo University of California, San Diego, Michael B. James University of California, San Diego, David Justo University of California, San Diego, Jiaxiao Zhou University of California, San Diego, Ziteng Wang University of California, San Diego, Ranjit Jhala University of California, San Diego, Nadia Polikarpova University of California, San Diego
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Synthesizing Replacement Classes
Research Papers
Malavika Samak CSAIL, MIT, Deokhwan Kim CSAIL, MIT, Martin C. Rinard MIT
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Gradual Typing / Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Jeremy G. Siek Indiana University, USA
14:00
21m
Talk
What is Decidable about Gradual Types?
Research Papers
Zeina Migeed University of California, Los Angeles, Jens Palsberg University of California, Los Angeles
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Graduality and Parametricity: Together Again for the First Time
Research Papers
Max S. New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USA
Link to publication DOI Media Attached
14:43
21m
Talk
Does Blame Shifting Work?
Research Papers
Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robert Bruce Findler Northwestern University, USA, Christos Dimoulas PLT @ Northwestern University
Link to publication DOI Media Attached
15:35 - 16:40
Concurrency / MemoryResearch Papers at Ile de France III (IDF III)
Chair(s): Susmit Sarkar University of St. Andrews
15:35
21m
Talk
Persistency Semantics of the Intel-x86 Architecture
Research Papers
Azalea Raad MPI-SWS, Germany, John Wickerson Imperial College London, Gil Neiger Intel Corporation, Viktor Vafeiadis MPI-SWS, Germany
Link to publication DOI Media Attached
15:56
21m
Talk
Reductions for Safety Proofs
Research Papers
Azadeh Farzan University of Toronto, Anthony Vandikas University of Toronto
Link to publication DOI Media Attached
16:18
21m
Talk
RustBelt Meets Relaxed Memory
Research Papers
Hoang-Hai Dang MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Jan-Oliver Kaiser MPI-SWS, Derek Dreyer MPI-SWS
Link to publication DOI Media Attached

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
SynthesisResearch Papers at Ile de France III (IDF III)
Chair(s): Mohsen Lesani University of California, Riverside
10:30
21m
Talk
Synthesis of Coordination Programs from Linear Temporal Specifications
Research Papers
Suguman Bansal Rice University, USA, Kedar Namjoshi Bell Labs, Nokia, Yaniv Sa'ar Nokia Bell Labs, Kfar Saba, Israel
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
Augmented Example-based Synthesis using Relational Perturbation Properties
Research Papers
Shengwei An Purdue University, Rishabh Singh Google Brain, Sasa Misailovic University of Illinois at Urbana-Champaign, Roopsha Samanta Purdue University
Link to publication DOI Media Attached File Attached
11:13
21m
Talk
Provenance-Guided Synthesis of Datalog Programs
Research Papers
Mukund Raghothaman University of Southern California, Jonathan Mendelson University of Pennsylvania, David Zhao The University of Sydney, Mayur Naik University of Pennsylvania, Bernhard Scholz University of Sydney, Australia
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Datalog, OO + Functional ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Brigitte Pientka McGill University
11:45
22m
Talk
Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper
Research Papers
Neel Krishnaswami Computer Laboratory, University of Cambridge, Michael Arntzenius University of Birmingham, UK
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Decomposition Diversity with Symmetric Data and Codata
Research Papers
David Binder University of Tübingen, Julian Jabs University of Tübingen, Ingo Skupin University of Tübingen, Klaus Ostermann University of Tübingen, Germany
Link to publication DOI Media Attached
14:00 - 15:05
Abstract InterpretationResearch Papers at Ile de France III (IDF III)
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
14:00
21m
Talk
Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations
Research Papers
Roberto Bruni University of Pisa, Roberto Giacobazzi University of Verona and IMDEA Software Institute, Roberta Gori University of Pisa, Isabel Garcia-Contreras IMDEA Software Institute, Dusko Pavlovic University of Hawaii
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Abstract Interpretation of Distributed Network Control Planes
Research Papers
Ryan Beckett Microsoft Research, Aarti Gupta Princeton University, Ratul Mahajan University of Washington, Intentionet, David Walker Princeton University
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Deterministic Parallel Fixpoint Computation
Research Papers
Sung Kook Kim University of California, Davis, Arnaud J. Venet Facebook, Aditya V. Thakur University of California, Davis
Link to publication DOI Pre-print Media Attached File Attached
15:35 - 16:40
Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III)
Chair(s): Ohad Kammar University of Edinburgh
15:35
21m
Talk
A Language for Probabilistically Oblivious Computation
Research Papers
David Darais University of Vermont, Ian Sweet University of Maryland, Chang Liu Citadel Securities, Michael Hicks University of Maryland
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
PλωNK: Functional Probabilistic NetKAT
Research Papers
Alexander Vandenbroucke KU Leuven, Belgium, Tom Schrijvers KU Leuven
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Optimal Approximate Sampling From Discrete Probability Distributions
Research Papers
Feras Saad Massachusetts Institute of Technology, Cameron Freer Massachusetts Institute of Technology, Martin C. Rinard MIT, Vikash K. Mansinghka MIT
Link to publication DOI Media Attached File Attached

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III)
Chair(s): Sandrine Blazy Univ Rennes- IRISA
10:30
21m
Talk
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation
Research Papers
Mengqi Liu Yale University, Lionel Rieg Verimag, Zhong Shao Yale University, Ronghui Gu Columbia University, David Costanzo Yale University, Jung-Eun Kim Yale University, Man-Ki Yoon Yale University
Link to publication DOI Media Attached File Attached
10:51
21m
Talk
The High-Level Benefits of Low-Level Sandboxing
Research Papers
Michael Sammler MPI-SWS, Deepak Garg Max Planck Institute for Software Systems, Derek Dreyer MPI-SWS, Tadeusz Litak FAU Erlangen-Nuremberg, INF 8
Link to publication DOI Media Attached
11:13
21m
Talk
Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper
Research Papers
Li-yao Xia University of Pennsylvania, Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Gregory Malecha BedRock Systems, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania
Link to publication DOI Media Attached File Attached
11:45 - 12:30
Probabilistic Reasoning and VerificationResearch Papers at Ile de France III (IDF III)
Chair(s): Arthur Azevedo de Amorim Carnegie Mellon University, USA
11:45
22m
Talk
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
Research Papers
Peixin Wang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Yuxin Deng East China Normal University, Ming Xu East China Normal University
Link to publication DOI Media Attached
12:07
22m
Talk
Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification
Research Papers
Marcel Hark RWTH Aachen University, Germany, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Jürgen Giesl RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University
Link to publication DOI Media Attached File Attached
14:00 - 15:05
Language DesignResearch Papers at Ile de France III (IDF III)
Chair(s): Amin Timany imec-Distrinet KU-Leuven
14:00
21m
Talk
Stacked Borrows: An Aliasing Model for Rust
Research Papers
Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Executable Formal Semantics for the POSIX Shell
Research Papers
Michael Greenberg Pomona College, Austin J. Blatt Puppet Labs
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Disentanglement in Nested-Parallel Programs
Research Papers
Sam Westrick Carnegie Mellon University, Rohan Yadav Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Umut A. Acar Carnegie Mellon University
Link to publication DOI Media Attached File Attached
15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew W. Appel Princeton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine Blazy Univ Rennes- IRISA, Benjamin Gregoire INRIA, Rémi Hutin IRISA / ENS Rennes, Vincent Laporte Inria, David Pichardie Univ Rennes, ENS Rennes, IRISA, Alix Trieu Aarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju Song Seoul National University, Minki Cho Seoul National University, Dongjoo Kim Seoul National University, Yonghyun Kim Seoul National University, South Korea, Jeehoon Kang KAIST, Chung-Kil Hur Seoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy Bourke Inria / École normale supérieure, Lelio Brun ENS/Inria, Marc Pouzet École normale supérieure
Link to publication DOI Media Attached File Attached

Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Ile de France III (IDF III)

PLMW

Morning 1

PLMW

Morning 2

PLMW

Afternoon 1

PLMW

Afternoon 2

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:003011:003012:003013:003014:003015:003016:0030
Ile de France III (IDF III)

Research Papers

Complexity / Decision Procedures

Research Papers

Synthesis

Research Papers

Gradual Typing / Language Design

Research Papers

Concurrency / Memory

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:003011:003012:003013:003014:003015:003016:0030
Ile de France III (IDF III)

Research Papers

Synthesis

Research Papers

Datalog, OO + Functional Programming

Research Papers

Abstract Interpretation

Research Papers

Probabilistic Programming

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:003011:003012:003013:003014:003015:003016:0030
Ile de France III (IDF III)

Research Papers

Verification in Proof Assistants

Research Papers

Probabilistic Reasoning and Verification

Research Papers

Language Design

Research Papers

Verified & Secure Compilation

Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Ile de France III (IDF III)
PLMW
Opening
09:00 - 09:10
PLMWMentoring Event
How to Write Papers So People Can Read Them
09:10 - 10:00
PLMWMentoring Event
Making Progress Under Uncertainty in SMT Solving, Research, and Life
10:30 - 11:10
PLMWMentoring Event
Research as a collaborative effort
11:10 - 11:50
PLMWMentoring Event
Theorem provers are a P.L. researcher's best friend
11:50 - 12:30
PLMWMentoring Event
Panel
14:00 - 15:05
PLMWMentoring Event
How Can I Academia When My Brain Can't Even? Mental Health in Grad Scho ...
15:40 - 16:40
PLMW
Mini break
16:40 - 16:50
PLMWMentoring Event
Automated Program Verification using Abductive Reasoning
16:50 - 17:35

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Ile de France III (IDF III)
POPL Research Papers
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
10:30 - 10:51
POPL Research Papers
Complexity and Information in Invariant Inference
10:51 - 11:13
POPL Research Papers
Parameterized Verification under TSO is PSPACE-Complete
11:13 - 11:35
POPL Research Papers
Program Synthesis by Type-Guided Abstraction Refinement
11:45 - 12:07
POPL Research Papers
Synthesizing Replacement Classes
12:07 - 12:30
POPL Research Papers
What is Decidable about Gradual Types?
14:00 - 14:21
POPL Research Papers
Graduality and Parametricity: Together Again for the First Time
14:21 - 14:43
POPL Research Papers
Does Blame Shifting Work?
14:43 - 15:05
POPL Research Papers
Persistency Semantics of the Intel-x86 Architecture
15:35 - 15:56
POPL Research Papers
Reductions for Safety Proofs
15:56 - 16:18
POPL Research Papers
RustBelt Meets Relaxed Memory
16:18 - 16:40

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Ile de France III (IDF III)
POPL Research Papers
Synthesis of Coordination Programs from Linear Temporal Specifications
10:30 - 10:51
POPL Research Papers
Augmented Example-based Synthesis using Relational Perturbation Properties
10:51 - 11:13
POPL Research Papers
Provenance-Guided Synthesis of Datalog Programs
11:13 - 11:35
POPL Research PapersDistinguished Paper
Seminaïve Evaluation for a Higher-Order Functional Language
11:45 - 12:07
POPL Research Papers
Decomposition Diversity with Symmetric Data and Codata
12:07 - 12:30
POPL Research Papers
Abstract Extensionality: On the Properties of Incomplete Abstract Inter ...
14:00 - 14:21
POPL Research Papers
Abstract Interpretation of Distributed Network Control Planes
14:21 - 14:43
POPL Research Papers
Deterministic Parallel Fixpoint Computation
14:43 - 15:05
POPL Research Papers
A Language for Probabilistically Oblivious Computation
15:35 - 15:56
POPL Research Papers
PλωNK: Functional Probabilistic NetKAT
15:56 - 16:18
POPL Research Papers
Optimal Approximate Sampling From Discrete Probability Distributions
16:18 - 16:40

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Ile de France III (IDF III)
POPL Research Papers
Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedul ...
10:30 - 10:51
POPL Research Papers
The High-Level Benefits of Low-Level Sandboxing
10:51 - 11:13
POPL Research PapersDistinguished Paper
Interaction Trees: Representing Recursive and Impure Programs in Coq
11:13 - 11:35
POPL Research Papers
Proving Expected Sensitivity of Probabilistic Programs with Randomized ...
11:45 - 12:07
POPL Research Papers
Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Progr ...
12:07 - 12:30
POPL Research Papers
Stacked Borrows: An Aliasing Model for Rust
14:00 - 14:21
POPL Research Papers
Executable Formal Semantics for the POSIX Shell
14:21 - 14:43
POPL Research Papers
Disentanglement in Nested-Parallel Programs
14:43 - 15:05
POPL Research Papers
Formal Verification of a Constant-Time Preserving C Compiler
15:35 - 15:56
POPL Research Papers
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Ver ...
15:56 - 16:18
POPL Research Papers
Mechanized Semantics and Verified Compilation for a Dataflow Synchronou ...
16:18 - 16:40