POPL 2018
Sun 7 - Sat 13 January 2018 Los Angeles, California, United States
POPL 2018 (series) / Omni Hotel /

Room information: Watercourt

VenueOmni Hotel
Room nameWatercourt
Floor0
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

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Types and EffectsResearch 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 EvaluationResearch 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
TypesResearch 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 IResearch 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 boxResearch 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 TypesResearch 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 LanguagesResearch 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
ProbabilityResearch 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 StateResearch 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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Watercourt

Research Papers

Types and Effects

Research Papers

Interpretation and Evaluation

Research Papers

Types

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

Room10:003011:003012:003013:003014:003015:003016:0030
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

Room10:003011:003012:003013:003014:003015:003016:003017:0030
Watercourt

Research Papers

Dynamic Languages

Research Papers

Probability

Research Papers

Types for State

Wed 10 Jan

Displayed time zone: Tijuana, Baja California change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
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

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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