POPL 2018
Sun 7 - Sat 13 January 2018
Los Angeles, California, United States
Toggle navigation
Attending
Venue: Omni Hotel
Registration
Code of Conduct
Supporting POPL
Childcare
Students
Visa Support Letter
Accessibility
Remote Participation
Program
POPL Program
Your Program
Proceedings
Filter by Day
Sun 7 Jan
Mon 8 Jan
Tue 9 Jan
Wed 10 Jan
Thu 11 Jan
Fri 12 Jan
Sat 13 Jan
Tracks
POPL 2018
Research Papers
TutorialFest
Student Research Competition
Workshops
Artifact Evaluation
Student Volunteers
Co-hosted Conferences
CPP
CPP
CPP
VMCAI
Workshops
PPS
CoqPL
NetPL
Off the Beaten Track
PEPM
PLMW
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2018 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
TutorialFest
Student Research Competition
Workshops
Artifact Evaluation
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Invited Tutorial
Organizing Committee
Travel Grants
Program Committee
Workshops
PPS
Program Committee
CoqPL
Organizing Committee
Program Committee
NetPL
Organizing Committee
Off the Beaten Track
Organizing Committee
Program Committee
PEPM
Programme Committee
Steering Committee
PLMW
Speakers
Panelists
Organizers
PriSC
Program Committee
Organizing Committee
Co-hosted Symposia
PADL
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 2018
(
series
) /
Omni Hotel
/
Room information: Watercourt
Venue
Omni Hotel
Room name
Watercourt
Floor
0
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-08:00) Tijuana, Baja California
.
Use conference time zone: (GMT-08:00) Tijuana, Baja California
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-03: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-02: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+11: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
Wed 10 Jan
Displayed time zone:
Tijuana, Baja California
change
10:30 - 12:10
Types and Effects
Research Papers
at
Watercourt
Chair(s):
Neel Krishnaswami
Computer Laboratory, University of Cambridge
10:30
25m
Talk
Linear Haskell: practical linearity in a higher-order polymorphic language
Research Papers
Jean-Philippe Bernardy
University of Gothenburg
,
Mathieu Boespflug
Tweag I/O
,
Ryan R. Newton
Indiana University
,
Simon Peyton Jones
Microsoft Research
,
Arnaud Spiwack
Tweag I/O
Pre-print
File Attached
10:55
25m
Talk
Polyadic Approximations, Fibrations and Intersection Types
Research Papers
Damiano Mazza
CNRS
,
Luc Pellissier
,
Pierre Vial
11:20
25m
Talk
Handling fibred algebraic effects
Research Papers
Danel Ahman
Inria Paris
11:45
25m
Talk
Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Research Papers
Dariusz Biernacki
University of Wrocław
,
Maciej Piróg
University of Wrocław
,
Piotr Polesiuk
University of Wrocław
,
Filip Sieczkowski
University of Wrocław
13:40 - 15:20
Interpretation and Evaluation
Research Papers
at
Watercourt
Chair(s):
Atsushi Igarashi
Kyoto University, Japan
13:40
25m
Talk
Unifying Analytic and Statically-Typed Quasiquotes
Research Papers
Lionel Parreaux
EPFL
,
Antoine Voizard
University of Pennsylvannia
,
Amir Shaikhha
EPFL
,
Christoph E. Koch
EPFL
Pre-print
14:05
25m
Talk
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Research Papers
Matt Brown
UCLA
,
Jens Palsberg
University of California, Los Angeles (UCLA)
14:30
25m
Talk
Migrating Gradual Types
Research Papers
John Peter Campora
ULL Lafayette
,
Sheng Chen
University of Louisiana at Lafayette
,
Martin Erwig
Oregon State University
,
Eric Walkingshaw
Oregon State University
14:55
25m
Talk
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Research Papers
Casper Bach Poulsen
Delft University of Technology
,
Arjen Rouvoet
Delft University of Technology
,
Andrew Tolmach
Portland State University
,
Robbert Krebbers
Delft University of Technology
,
Eelco Visser
Delft University of Technology
DOI
Pre-print
15:50 - 17:30
Types
Research Papers
at
Watercourt
Chair(s):
Thorsten Altenkirch
University of Nottingham
15:50
25m
Talk
A Principled approach to Ornamentation in ML
Research Papers
Thomas Williams
Inria
,
Didier Rémy
Inria
16:15
25m
Talk
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Research Papers
William J. Bowman
Northeastern University, USA
,
Youyou Cong
Ochanomizu University, Japan
,
Nick Rioux
Northeastern University, USA
,
Amal Ahmed
Northeastern University, USA
Link to publication
DOI
Pre-print
16:40
25m
Talk
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
Research Papers
Ondřej Kunčar
Technische Universität München, Germany
,
Andrei Popescu
Middlesex University, London
17:05
25m
Talk
Univalent Higher Categories via Complete Semi-Segal Types
Research Papers
Paolo Capriotti
University of Nottingham
,
Nicolai Kraus
University of Nottingham
Thu 11 Jan
Displayed time zone:
Tijuana, Baja California
change
10:30 - 12:10
Program Analysis I
Research Papers
at
Watercourt
Chair(s):
Tachio Terauchi
Waseda University
10:30
25m
Talk
Inference of Static Semantics for Incomplete C Programs
Research Papers
Leandro T. C. Melo
UFMG
,
Rodrigo Geraldo Ribeiro
UFOP
,
Marcus Rodrigues de Araújo
UFMG
,
Fernando Magno Quintão Pereira
UFMG
Pre-print
10:55
25m
Talk
Optimal Dyck Reachability for Data-dependence and Alias Analysis
Research Papers
Krishnendu Chatterjee
IST Austria
,
Andreas Pavlogiannis
IST Austria
,
Bhavya Choudhary
IIT Bombay
11:20
25m
Talk
Data-centric Dynamic Partial Order Reduction
Research Papers
Marek Chalupa
Masaryk University
,
Krishnendu Chatterjee
IST Austria
,
Andreas Pavlogiannis
IST Austria
,
Kapil Vaidya
IIT Bombay
,
Nishant Sinha
IBM Research
11:45
25m
Talk
Analytical Modeling of Cache Behavior for Affine Programs
Research Papers
Wenlei Bao
Ohio State University
,
Sriram Krishnamoorthy
Pacific Northwest National Laboratories
,
Louis-Noël Pouchet
Colorado State University
,
P. Sadayappan
Ohio State University
13:40 - 15:20
Outside the box
Research Papers
at
Watercourt
Chair(s):
Lars Birkedal
Aarhus University
13:40
25m
Talk
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Research Papers
Siddharth Krishna
New York University
,
Dennis Shasha
New York University
,
Thomas Wies
New York University
14:05
25m
Talk
Parametricity versus the Universal Type
Research Papers
Dominique Devriese
KU Leuven
,
Marco Patrignani
Saarland University, CISPA
,
Frank Piessens
KU Leuven
14:30
25m
Talk
Linearity in Higher-Order Recursion Schemes
Research Papers
Pierre Clairambault
CNRS & ENS Lyon
,
Charles Grellois
INRIA Sophia Antipolis & Aix-Marseille Université
,
Andrzej Murawski
University of Oxford
14:55
25m
Talk
Symbolic Types for Lenient Symbolic Execution
Research Papers
Stephen Chang
Northeastern University
,
Alex Knauth
Northeastern University
,
Emina Torlak
University of Washington
15:50 - 16:40
Dependent Types
Research Papers
at
Watercourt
Chair(s):
Karl Crary
Carnegie Mellon University
15:50
25m
Talk
Up-to Techniques Using Sized Types
Research Papers
Nils Anders Danielsson
University of Gothenburg, Chalmers University of Technology
16:15
25m
Talk
Decidability of Conversion for Type Theory in Type Theory
Research Papers
Andreas Abel
Gothenburg University
,
Joakim Öhman
IMDEA Software Institute
,
Andrea Vezzosi
Chalmers University of Technology
Fri 12 Jan
Displayed time zone:
Tijuana, Baja California
change
10:30 - 12:10
Dynamic Languages
Research Papers
at
Watercourt
Chair(s):
Jean Yang
Carnegie Mellon University
10:30
25m
Talk
Correctness of Speculative Optimizations with Dynamic Deoptimization
Research Papers
Olivier Flückiger
Northeastern University, USA
,
Gabriel Scherer
Northeastern University, USA
,
Ming-Ho Yee
Northeastern University, USA
,
Aviral Goel
Northeastern University
,
Amal Ahmed
Northeastern University, USA
,
Jan Vitek
Northeastern University
DOI
Pre-print
10:55
25m
Talk
JaVerT: JavaScript Verification Toolchain
Research Papers
José Fragoso Santos
Imperial College London
,
Petar Maksimović
Imperial College London
,
Daiva Naudžiūnienė
Imperial College London
,
Thomas Wood
Imperial College London
,
Philippa Gardner
Imperial College London
11:20
25m
Talk
Soft Contract Verification for Higher-order Stateful Programs
Research Papers
Phúc C. Nguyễn
University of Maryland
,
Thomas Gilray
University of Maryland
,
Sam Tobin-Hochstadt
Indiana University
,
David Van Horn
University of Maryland
11:45
25m
Talk
Collapsing Towers of Interpreters
Research Papers
Nada Amin
University of Cambridge
,
Tiark Rompf
Purdue University
13:40 - 15:20
Probability
Research Papers
at
Watercourt
Chair(s):
Lars Birkedal
Aarhus University
13:40
25m
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
Gilles Barthe
IMDEA Software Institute
,
Thomas Espitau
Universite Pierre et Marie Curie
,
Benjamin Gregoire
INRIA
,
Justin Hsu
University College London
,
Pierre-Yves Strub
Ecole Polytechnique
14:05
25m
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws Albarghouthi
University of Wisconsin-Madison
,
Justin Hsu
University College London
14:30
25m
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas Ehrhard
CNRS and University Paris Diderot
,
Michele Pagani
University Paris Diderot
,
Christine Tasson
University Paris Diderot
14:55
25m
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
Adam Ścibior
University of Cambridge and MPI Tuebingen
,
Ohad Kammar
University of Oxford
,
Matthijs Vákár
University of Oxford
,
Sam Staton
University of Oxford
,
Hongseok Yang
University of Oxford
,
Yufei Cai
University of Tuebingen
,
Klaus Ostermann
University of Tuebingen
,
Sean Moss
University of Oxford
,
Chris Heunen
University of Edinburgh
,
Zoubin Ghahramani
University of Cambridge
15:50 - 17:05
Types for State
Research Papers
at
Watercourt
Chair(s):
Neel Krishnaswami
Computer Laboratory, University of Cambridge
15:50
25m
Talk
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Research Papers
Amin Timany
imec-Distrinet KU-Leuven
,
Leo Stefanesco
ENS Lyon
,
Morten Krogh-Jespersen
Aarhus University
,
Lars Birkedal
Aarhus University
16:15
25m
Talk
Recalling a Witness: Foundations and Applications of Monotonic State
Research Papers
Danel Ahman
Inria Paris
,
Cédric Fournet
Microsoft Research
,
Cătălin Hriţcu
Inria Paris
,
Kenji Maillard
Inria Paris and ENS Paris
,
Aseem Rastogi
Microsoft Research
,
Nikhil Swamy
Microsoft Research
Pre-print
16:40
25m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
Research Papers
Ralf Jung
MPI-SWS
,
Jacques-Henri Jourdan
CNRS, LRI, Université Paris-Sud
,
Robbert Krebbers
Delft University of Technology
,
Derek Dreyer
MPI-SWS
Wed 10 Jan
Displayed time zone:
Tijuana, Baja California
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Watercourt
Research Papers
Types and Effects
Research Papers
Interpretation and Evaluation
Research Papers
Types
Thu 11 Jan
Displayed time zone:
Tijuana, Baja California
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
Watercourt
Research Papers
Program Analysis I
Research Papers
Outside the box
Research Papers
Dependent Types
Fri 12 Jan
Displayed time zone:
Tijuana, Baja California
change
Room
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Watercourt
Research Papers
Dynamic Languages
Research Papers
Probability
Research Papers
Types for State
Wed 10 Jan
Displayed time zone:
Tijuana, Baja California
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Watercourt
POPL Research Papers
Linear Haskell: practical linearity in a higher-order polymorphic language
10:30 - 10:55
POPL Research Papers
Polyadic Approximations, Fibrations and Intersection Types
10:55 - 11:20
POPL Research Papers
Handling fibred algebraic effects
11:20 - 11:45
POPL Research Papers
Handle with Care: Relational Interpretation of Algebraic Effects and Ha ...
11:45 - 12:10
POPL Research Papers
Unifying Analytic and Statically-Typed Quasiquotes
13:40 - 14:05
POPL Research Papers
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
14:05 - 14:30
POPL Research Papers
Migrating Gradual Types
14:30 - 14:55
POPL Research Papers
Intrinsically-Typed Definitional Interpreters for Imperative Languages
14:55 - 15:20
POPL Research Papers
A Principled approach to Ornamentation in ML
15:50 - 16:15
POPL Research Papers
Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
16:15 - 16:40
POPL Research Papers
Safety and Conservativity of Definitions in HOL and Isabelle/HOL
16:40 - 17:05
POPL Research Papers
Univalent Higher Categories via Complete Semi-Segal Types
17:05 - 17:30
Thu 11 Jan
Displayed time zone:
Tijuana, Baja California
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
Watercourt
POPL Research Papers
Inference of Static Semantics for Incomplete C Programs
10:30 - 10:55
POPL Research Papers
Optimal Dyck Reachability for Data-dependence and Alias Analysis
10:55 - 11:20
POPL Research Papers
Data-centric Dynamic Partial Order Reduction
11:20 - 11:45
POPL Research Papers
Analytical Modeling of Cache Behavior for Affine Programs
11:45 - 12:10
POPL Research Papers
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
13:40 - 14:05
POPL Research Papers
Parametricity versus the Universal Type
14:05 - 14:30
POPL Research Papers
Linearity in Higher-Order Recursion Schemes
14:30 - 14:55
POPL Research Papers
Symbolic Types for Lenient Symbolic Execution
14:55 - 15:20
POPL Research Papers
Up-to Techniques Using Sized Types
15:50 - 16:15
POPL Research Papers
Decidability of Conversion for Type Theory in Type Theory
16:15 - 16:40
Fri 12 Jan
Displayed time zone:
Tijuana, Baja California
change
Room
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Watercourt
POPL Research Papers
Correctness of Speculative Optimizations with Dynamic Deoptimization
10:30 - 10:55
POPL Research Papers
JaVerT: JavaScript Verification Toolchain
10:55 - 11:20
POPL Research Papers
Soft Contract Verification for Higher-order Stateful Programs
11:20 - 11:45
POPL Research Papers
Collapsing Towers of Interpreters
11:45 - 12:10
POPL Research Papers
Proving expected sensitivity of probabilistic programs
13:40 - 14:05
POPL Research Papers
Synthesizing Coupling Proofs of Differential Privacy
14:05 - 14:30
POPL Research Papers
Measurable cones and stable, measurable functions
14:30 - 14:55
POPL Research Papers
Denotational validation of higher-order Bayesian inference
14:55 - 15:20
POPL Research Papers
A Logical Relation for Monadic Encapsulation of State: Proving contextu ...
15:50 - 16:15
POPL Research Papers
Recalling a Witness: Foundations and Applications of Monotonic State
16:15 - 16:40
POPL Research Papers
RustBelt: Securing the Foundations of the Rust Programming Language
16:40 - 17:05
x
Mon 9 Dec 10:28