Write a Blog >>
POPL 2020
Sun 19 - Sat 25 January 2020
New Orleans, Louisiana, United States
Toggle navigation
Attending
Venue: JW Marriott New Orleans
Restaurant: Palace Cafe
Registration
Online Participation
Travel to the USA
Mentoring Events
Information for Students
Code of Conduct
Supporting POPL
Accessibility
SIGPLAN CARES
Program
Complete Program
Your Program
Filter by Day
Sun 19 Jan
Mon 20 Jan
Tue 21 Jan
Wed 22 Jan
Thu 23 Jan
Fri 24 Jan
Sat 25 Jan
Tracks
POPL 2020
Research Papers
Artifact Evaluation
Student Research Competition
Workshops and Co-located Events
TutorialFest
POPLmark 15 Year Retrospective Panel
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Co-hosted Conferences
CPP
VMCAI
Workshops
ADSL
CoqPL
HASE
LAFI
(né PPS)
PEPM
PLMW
PLanQC
PriSC
PriSC
Principles of Secure Compilation
- Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
WGT
Co-hosted Symposia
PADL
Organization
POPL 2020 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
Artifact Evaluation
Student Research Competition
TutorialFest
POPLmark 15 Year Retrospective Panel
Panel
Organizing Committee
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact-Evaluation Committee
Steering Committee
Workshops
ADSL
Organizing Committee
Program Committee
CoqPL
Invited speakers
Organizing Committee
Program Committee
HASE
Organizing Committee
Program Committee
LAFI
Program Committee
Steering Committee
PEPM
PC Chairs
Program Committee
PLMW
Organizing Committee
Invited speakers
Panelists
PLanQC
Organizing Committee
Program Committee
PriSC
Program Committee
Steering Committee
WGT
Organizing Committee
Program Committee
Co-hosted Symposia
PADL
Program Chairs
Program Committee
Publicity Chair
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2020
(
series
) /
JW Marriott New Orleans
/
Room information: Ile de France III (IDF III)
Venue
JW Marriott New Orleans
Room name
Ile de France III (IDF III)
Floor
3
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-06:00) Saskatchewan, Central America
.
Use conference time zone: (GMT-06:00) Saskatchewan, Central America
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Tue 21 Jan
Displayed time zone:
Saskatchewan, Central America
change
09:00 - 10:00
Morning 1
PLMW
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 Them
Mentoring Event
PLMW
Derek Dreyer
MPI-SWS
File Attached
10:30 - 12:30
Morning 2
PLMW
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 Life
Mentoring Event
PLMW
Lindsey Kuper
University of California, Santa Cruz
Media Attached
11:10
40m
Talk
Research as a collaborative effort
Mentoring Event
PLMW
Marco Gaboardi
Boston University
Media Attached
File Attached
11:50
40m
Talk
Theorem provers are a P.L. researcher's best friend
Mentoring Event
PLMW
Xavier Leroy
Collège de France
Media Attached
File Attached
14:00 - 15:05
Afternoon 1
PLMW
at
Ile de France III (IDF III)
Chair(s):
Justin Hsu
University of Wisconsin-Madison, USA
14:00
65m
Talk
Panel
Mentoring 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 2
PLMW
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 Beyond
Mentoring Event
PLMW
Kenny Foner
Galois
Media Attached
16:40
10m
Coffee break
Mini break
PLMW
16:50
45m
Talk
Automated Program Verification using Abductive Reasoning
Mentoring 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 Procedures
Research 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
Synthesis
Research 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 Design
Research 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 / Memory
Research 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
Synthesis
Research 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 Programming
Research 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 Language
Distinguished 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 Interpretation
Research 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 Programming
Research 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 Assistants
Research 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 Coq
Distinguished 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 Verification
Research 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 Design
Research 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 Compilation
Research 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
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
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
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
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
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
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
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
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
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Ile de France III (IDF III)
PLMW
Opening
09:00 - 09:10
PLMW
Mentoring Event
How to Write Papers So People Can Read Them
09:10 - 10:00
PLMW
Mentoring Event
Making Progress Under Uncertainty in SMT Solving, Research, and Life
10:30 - 11:10
PLMW
Mentoring Event
Research as a collaborative effort
11:10 - 11:50
PLMW
Mentoring Event
Theorem provers are a P.L. researcher's best friend
11:50 - 12:30
PLMW
Mentoring Event
Panel
14:00 - 15:05
PLMW
Mentoring 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
PLMW
Mentoring Event
Automated Program Verification using Abductive Reasoning
16:50 - 17:35
Wed 22 Jan
Displayed time zone:
Saskatchewan, Central America
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
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
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
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 Papers
Distinguished 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
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
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 Papers
Distinguished 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
x
Sun 8 Sep 01:35