Powered by
Conference Publishing Consulting

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

ICFP 2015 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Chairs' Welcome
Organization
Sponsors

Keynote 1

Program Synthesis: Opportunities for the Next Decade
Rastislav Bodik
(University of Washington, USA)
Publisher's Version Article Search

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)
Publisher's Version Article Search Info
An Optimizing Compiler for a Purely Functional Web-Application Language
Adam Chlipala
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search

Session 2: Types

1ML – Core and Modules United (F-ing First-Class Modules)
Andreas Rossberg
(Google, Germany)
Publisher's Version Article Search
Bounded Refinement Types
Niki Vazou, Alexander Bakst, and Ranjit Jhala
(University of California at San Diego, USA)
Publisher's Version Article Search Video

Session 3: Miscellaneous

Applicative Bidirectional Programming with Lenses
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Kent, UK)
Publisher's Version Article Search
Hygienic Resugaring of Compositional Desugaring
Justin Pombrio and Shriram Krishnamurthi
(Brown University, USA)
Publisher's Version Article Search
XQuery and Static Typing: Tackling the Problem of Backward Axes
Pierre Genevès and Nils Gesbert
(University of Grenoble, France; CNRS, France; INRIA, France)
Publisher's Version Article Search

Session 4: Foundations I

Noninterference for Free
William J. Bowman and Amal Ahmed
(Northeastern University, USA)
Publisher's Version Article Search
Algebras and Coalgebras in the Light Affine Lambda Calculus
Marco Gaboardi and Romain Péchoux
(University of Dundee, UK; University of Lorraine, France)
Publisher's Version Article Search
Structures for Structural Recursion
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola
(University of Oregon, USA)
Publisher's Version Article Search Info

Session 5: Cost Analysis

Denotational Cost Semantics for Functional Languages with Inductive Types
Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa
(Wesleyan University, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Keynote 2

Functional Programming and Hardware Design: Still Interesting after All These Years
Mary Sheeran
(Chalmers University of Technology, Sweden)
Publisher's Version Article Search

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Adaptive Lock-Free Maps: Purely-Functional to Scalable
Ryan R. Newton, Peter P. Fogg, and Ali Varamesh
(Indiana University, USA)
Publisher's Version Article Search
Partial Aborts for Transactions via First-Class Continuations
Matthew Le and Matthew Fluet
(Rochester Institute of Technology, USA)
Publisher's Version Article Search

Session 8: Foundations II

Which Simple Types Have a Unique Inhabitant?
Gabriel Scherer and Didier Rémy
(INRIA, France)
Publisher's Version Article Search
Elaborating Evaluation-Order Polymorphism
Joshua Dunfield
(University of British Columbia, Canada)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Session 9: Information Flow

Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell
Alejandro Russo
(Chalmers University of Technology, Sweden)
Publisher's Version Article Search
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Certified Symbolic Management of Financial Multi-party Contracts
Patrick Bahr, Jost Berthold, and Martin Elsman
(University of Copenhagen, Denmark; Commonwealth Bank of Australia, Australia)
Publisher's Version Article Search Info
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)
Publisher's Version Article Search

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)
Publisher's Version Article Search
Functional Pearl: A Smart View on Datatypes
Mauro Jaskelioff and Exequiel Rivas
(CIFASIS-CONICET, Argentina; Universidad Nacional de Rosario, Argentina)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Session 12: Contracts

Blame Assignment for Higher-Order Contracts with Intersection and Union
Matthias Keil and Peter Thiemann
(University of Freiburg, Germany)
Publisher's Version Article Search
Expressing Contract Monitors as Patterns of Communication
Cameron Swords, Amr Sabry, and Sam Tobin-Hochstadt
(Indiana University, USA)
Publisher's Version Article Search
Learning Refinement Types
He Zhu, Aditya V. Nori, and Suresh Jagannathan
(Purdue University, USA; Microsoft Research, USA)
Publisher's Version Article Search

Session 13: Type Checking

Practical SMT-Based Type Error Localization
Zvonimir Pavlinovic, Tim King, and Thomas Wies
(New York University, USA; VERIMAG, France)
Publisher's Version Article Search
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)
Publisher's Version Article Search

proc time: 1.61