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 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 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 doi:

Session 2: Types

Bounded Refinement Types
Niki Vazou, Alexander Bakst, and Ranjit Jhala
(University of California at San Diego, USA)
Article: icfp15main-main041-p 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 doi:

Hygienic Resugaring of Compositional Desugaring
Justin Pombrio and Shriram Krishnamurthi
(Brown University, USA)
Article: icfp15main-main075-p 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 doi:

Session 4: Foundations I

Noninterference for Free
William J. Bowman and Amal Ahmed
(Northeastern University, USA)
Article: icfp15main-main003-p 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 doi:

Structures for Structural Recursion
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola
(University of Oregon, USA)
Article: icfp15main-main095-p 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 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 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 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 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 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 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 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 doi:

Partial Aborts for Transactions via First-Class Continuations
Matthew Le and Matthew Fluet
(Rochester Institute of Technology, USA)
Article: icfp15main-main021-p doi:

Session 8: Foundations II

Elaborating Evaluation-Order Polymorphism
Joshua Dunfield
(University of British Columbia, Canada)
Article: icfp15main-main040-p doi:

Session 9: Information Flow

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 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 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 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 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 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 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 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 doi:

Expressing Contract Monitors as Patterns of Communication
Cameron Swords, Amr Sabry, and Sam Tobin-Hochstadt
(Indiana University, USA)
Article: icfp15main-main032-p doi:

Learning Refinement Types
He Zhu, Aditya V. Nori, and Suresh Jagannathan
(Purdue University, USA; Microsoft Research, USA)
Article: icfp15main-main120-p 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 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 doi: