ICFP 2015 – Proceedings

20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), August 31 – September 2, 2015, Vancouver, BC, Canada

Frontmatter

Keynote 1

Program Synthesis: Opportunities for the Next Decade
Rastislav Bodik
(University of Washington, USA)
Article: icfp15main-keynotesid1-p (type: Invited Talk Abstract (1 page)) doi:

Session 1: Compilers

Functional Pearl: A SQL to C Compiler in 500 Lines of Code
Tiark Rompf and Nada Amin
(Purdue University, USA; EPFL, Switzerland)
Article: icfp15main-main085-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

An Optimizing Compiler for a Purely Functional Web-Application Language
Adam Chlipala
(Massachusetts Institute of Technology, USA)
Article: icfp15main-main029-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Pycket: A Tracing JIT for a Functional Language
Spenser Bauman, Carl Friedrich Bolz, Robert Hirschfeld, Vasily Kirilichev, Tobias Pape, Jeremy G. Siek, and Sam Tobin-Hochstadt
(Indiana University, USA; Kings College London, UK; HPI, Germany)
Article: icfp15main-main028-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 2: Types

1ML – Core and Modules United (F-ing First-Class Modules)
Andreas Rossberg
(Google, Germany)
Article: icfp15main-main025-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Bounded Refinement Types
Niki Vazou, Alexander Bakst, and Ranjit Jhala
(University of California at San Diego, USA)
Article: icfp15main-main041-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 3: Miscellaneous

Applicative Bidirectional Programming with Lenses
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Kent, UK)
Article: icfp15main-main058-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Hygienic Resugaring of Compositional Desugaring
Justin Pombrio and Shriram Krishnamurthi
(Brown University, USA)
Article: icfp15main-main075-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

XQuery and Static Typing: Tackling the Problem of Backward Axes
Pierre Genevès and Nils Gesbert
(University of Grenoble, France; CNRS, France; INRIA, France)
Article: icfp15main-main043-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 4: Foundations I

Noninterference for Free
William J. Bowman and Amal Ahmed
(Northeastern University, USA)
Article: icfp15main-main003-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Algebras and Coalgebras in the Light Affine Lambda Calculus
Marco Gaboardi and Romain Péchoux
(University of Dundee, UK; University of Lorraine, France)
Article: icfp15main-main083-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Structures for Structural Recursion
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola
(University of Oregon, USA)
Article: icfp15main-main095-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 5: Cost Analysis

Denotational Cost Semantics for Functional Languages with Inductive Types
Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa
(Wesleyan University, USA)
Article: icfp15main-main055-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order
Martin Avanzini, Ugo Dal Lago, and Georg Moser
(University of Bologna, Italy; INRIA, France; University of Innsbruck, Austria)
Article: icfp15main-main069-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Keynote 2

Functional Programming and Hardware Design: Still Interesting after All These Years
Mary Sheeran
(Chalmers University of Technology, Sweden)
Article: icfp15main-keynotesid2-p (type: Invited Talk Abstract (1 page)) doi:

Session 6: Theorem Provers

Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language
Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis
(MPI-SWS, Germany; Seoul National University, South Kroea; University of Glasgow, UK)
Article: icfp15main-main112-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading
Beta Ziliani and Matthieu Sozeau
(MPI-SWS, Germany; INRIA, France; University of Paris Diderot, France)
Article: icfp15main-main061-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Foundational Extensible Corecursion: A Proof Assistant Perspective
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel
(INRIA, France; LORIA, France; Middlesex University, UK; TU München, Germany)
Article: icfp15main-main001-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 7: Parallelism

Generating Performance Portable Code using Rewrite Rules: From High-Level Functional Expressions to High-Performance OpenCL Code
Michel Steuwer, Christian Fensch, Sam Lindley, and Christophe Dubach
(University of Edinburgh, UK; University of Münster, Germany; Heriot-Watt University, UK)
Article: icfp15main-main073-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Adaptive Lock-Free Maps: Purely-Functional to Scalable
Ryan R. Newton, Peter P. Fogg, and Ali Varamesh
(Indiana University, USA)
Article: icfp15main-main004-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Partial Aborts for Transactions via First-Class Continuations
Matthew Le and Matthew Fluet
(Rochester Institute of Technology, USA)
Article: icfp15main-main021-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 8: Foundations II

Which Simple Types Have a Unique Inhabitant?
Gabriel Scherer and Didier Rémy
(INRIA, France)
Article: icfp15main-main080-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Elaborating Evaluation-Order Polymorphism
Joshua Dunfield
(University of British Columbia, Canada)
Article: icfp15main-main040-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem
Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann
(University of Tübingen, Germany)
Article: icfp15main-main101-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 9: Information Flow

Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell
Alejandro Russo
(Chalmers University of Technology, Sweden)
Article: icfp15main-main077-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell
Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo
(Chalmers University of Technology, Sweden; Microsoft Research, UK)
Article: icfp15main-main082-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 10: Domain-Specific Languages

Practical Principled FRP: Forget the Past, Change the Future, FRPNow!
Atze van der Ploeg and Koen Claessen
(Chalmers University of Technology, Sweden)
Article: icfp15main-main065-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Certified Symbolic Management of Financial Multi-party Contracts
Patrick Bahr, Jost Berthold, and Martin Elsman
(University of Copenhagen, Denmark; Commonwealth Bank of Australia, Australia)
Article: icfp15main-main051-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

A Fast Compiler for NetKAT
Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha
(Cornell University, USA; Inhabited Type, USA; University of Massachusetts at Amherst, USA)
Article: icfp15main-main090-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 11: Data Structures

RRB Vector: A Practical General Purpose Immutable Sequence
Nicolas Stucki, Tiark Rompf, Vlad Ureche, and Phil Bagwell
(EPFL, Switzerland; Purdue University, USA)
Article: icfp15main-main027-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Functional Pearl: A Smart View on Datatypes
Mauro Jaskelioff and Exequiel Rivas
(CIFASIS-CONICET, Argentina; Universidad Nacional de Rosario, Argentina)
Article: icfp15main-main033-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Efficient Communication and Collection with Compact Normal Forms
Edward Z. Yang, Giovanni Campagna, Ömer S. Ağacan, Ahmed El-Hassany, Abhishek Kulkarni, and Ryan R. Newton
(Stanford University, USA; Indiana University, USA)
Article: icfp15main-main009-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 12: Contracts

Blame Assignment for Higher-Order Contracts with Intersection and Union
Matthias Keil and Peter Thiemann
(University of Freiburg, Germany)
Article: icfp15main-main024-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Expressing Contract Monitors as Patterns of Communication
Cameron Swords, Amr Sabry, and Sam Tobin-Hochstadt
(Indiana University, USA)
Article: icfp15main-main032-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Learning Refinement Types
He Zhu, Aditya V. Nori, and Suresh Jagannathan
(Purdue University, USA; Microsoft Research, USA)
Article: icfp15main-main120-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

Session 13: Type Checking

Practical SMT-Based Type Error Localization
Zvonimir Pavlinovic, Tim King, and Thomas Wies
(New York University, USA; VERIMAG, France)
Article: icfp15main-main113-p (type: Full Paper (13 pages + 1 optional page with costs)) doi:

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness
Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones
(Ghent University, Belgium; KU Leuven, Belgium; Microsoft Research, UK)
Article: icfp15main-main052-p (type: Full Paper (13 pages + 1 optional page with costs)) doi: