Accepted papers

Foundational Extensible Corecursion: A Proof Assistant Perspective
Jasmin Christian Blanchette (Inria & LORIA, Nancy), Andrei Popescu (Middlesex University), and Dmitriy Traytel (TU München)
Noninterference for Free
William J. Bowman (Northeastern University CCIS) and Amal Ahmed (Northeastern University CCIS)
Adaptive Lock-Free Data: Purely-Functional to Scalable
Peter Fogg (Indiana University), Ali Varamesh (Indiana University), and Ryan R. Newton (Indiana University)
Efficient Communication and Collection with Compact Normal Forms
Abhishek Kulkarni (Indiana University), Ahmed El-Hassany (Indiana University), Edward Z. Yang (Stanford University), Giovanni Campagna (Stanford University), Ryan Newton (Indiana University), and Ömer S. Ağacan (Indiana University)
Partial Aborts for Transactions via First-Class Continuations
Matthew Le (Rochester Institute of Technology) and Matthew Fluet (Rochester Institute of Technology)
Blame Assignment for Higher-Order Contracts with Intersection and Union
Matthias Keil (University of Freiburg) and Peter Thiemann (University of Freiburg)
1ML - Core and modules united (F-ing first-class modules)
Andreas Rossberg (Google)
RRB Vector: A Practical General Purpose Immutable Sequence
Nicolas Stucki (EPFL, Switzerland), Tiark Rompf (Purdue University), and Vlad Ureche (EPFL, Switzerland)
Pycket: A Tracing JIT For a Functional Language
Spenser Bauman (Indiana University), Carl Friedrich Bolz (Kings College, London), Robert Hirschfeld (Hassno-Plattner-Institut, Potsdam), Vasily Krilichev (Hassno-Plattner-Institut, Potsdam), Tobias Pape (Hassno-Plattner-Institut, Potsdam), Jeremy G. Siek (Indiana University), and Sam Tobin-Hochstadt (Indiana University)
An Optimizing Compiler for a Purely Functional Web-Application Language
Adam Chlipala (MIT CSAIL)
Expressing Contract Monitors as Patterns of Communication
Cameron Swords (Indiana University), Amr Sabry (Indiana University), and Sam Tobin-Hochstadt (Indiana University)
Functional Pearl: A Smart View on Datatypes
Mauro Jaskelioff (CIFASIS - CONICET) and Exequiel Rivas (CIFASIS - CONICET)
Elaborating Evaluation-Order Polymorphism
Joshua Dunfield (University of British Columbia)
Bounded Refinement Types
Niki Vazou (UC San Diego), Alexander Bakst (UC San Diego), and Ranjit Jhala (UC San Diego)
XQuery and Static Typing: Tackling the Problem of Backward Axes
Pierre Genevès (CNRS) and Nils Gesbert (Université Grenoble Alpes)
Certified Symbolic Management of Financial Multi-Party Contracts
Patrick Bahr (University of Copenhagen), Jost Berthold (University of Copenhagen), and Martin Elsman (University of Copenhagen)
GADTs meet their match
Georgios Karachalias (Ghent University), Tom Schrijvers (KU Leuven), Dimitrios Vytiniotis (Microsoft Research Cambridge), and Simon Peyton Jones (Microsoft Research Cambridge)
Denotational cost semantics for functional languages with inductive types
Norman Danner (Wesleyan University), Daniel R. Licata (Wesleyan University), and Ramyaa Ramyaa (Wesleyan University)
Bidirectional Programming in a More Applicative Style
Kazutaka Matsuda (The University of Tokyo) and Meng Wang (University of Kent)
A Predictable Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading
Beta Ziliani (MPI-SWS) and Matthieu Sozeau (Inria & PPS, Université Paris Diderot)
Practical Principled FRP: Forget the past, change the future, FRPNow!
Atze van der Ploeg (Chalmers University of Technology) and Koen Claessen (Chalmers University of Technology)
Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order
Martin Avanzini (University of Bologna, Italy & Inria, France), Ugo Dal Lago (University of Bologna, Italy & Inria, France), and Georg Moser (University of Innsbruck)
Generating Performance Portable Code using Rewrite Rules: From High-level Functional Expressions to High-Performance OpenCL Code
Michel Steuwer (The University of Edinburgh, UK), Christian Fensch (Heriot-Watt University, UK), Sam Lindley (The University of Edinburgh, UK), and Christophe Dubach (The University of Edinburgh, UK)
Hygienic Resugaring of Compositional Desugaring
Justin Pombrio (Brown University) and Shriram Krishnamurthi (Brown University)
Functional Pearl: Two can keep a secret, if one of them uses Haskell
Alejandro Russo (Chalmers University of Technology)
Which simple types have a unique inhabitant?
Gabriel Scherer (INRIA) and Didier Rèmy (INRIA)
HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell
Pablo Buiras (Chalmers University of Technology), Dimitrios Vytiniotis (Microsoft Research), and Alejandro Russo (Chalmers University of Technology)
Algebras and Coalgebras in the Light Affine Lambda Calculus
Marco Gaboardi (University of Dundee and Harvard University) and Romain Péchoux (Universitè de Lorraine)
Functional Pearl: A SQL to C Compiler in 500 Lines of Code
Tiark Rompf (Purdue University) and Nada Amin (EPFL)
A Fast Compiler for NetKAT
Steffen Smolka (Cornell University), Spiridon Eliopoulos (Inhabited Type), Nate Foster (Cornell University), and Arjun Guha (University of Massachusetts Amherst)
Structures for structural recursion
Paul Downen (University of Oregon), Philip Johnson-Freyd (University of Oregon), and Zena M. Ariola (University of Oregon)
Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem
Tillmann Rendel (University of Tübingen), Julia Trieflinger (University of Tübingen), and Klaus Ostermann (University of Tübingen)
Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language
Georg Neis (MPI-SWS, Germany), Chung-Kil Hur (Seoul National University), Jan-Oliver Kaiser (MPI-SWS, Germany), Craig McLaughlin (University of Glasgow), Derek Dreyer (MPI-SWS, Germany), and Viktor Vafeiadis (MPI-SWS, Germany)
Practical SMT-Based Type Error Localization
Zvonimir Pavlinovic (New York University), Tim King (Verimag), and Thomas Wies (New York University)
Learning Refinement Types
He Zhu (Purdue University), Aditya V. Nori (Microsoft Research), and Suresh Jagannathan (Purdue University)