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
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
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
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 K. Moss University of Cambridge, 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

Thu 11 Jan

Displayed time zone: Tijuana, Baja California change

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change