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)

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

Session 2: Types

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

Session 3: Miscellaneous

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

Session 4: Foundations I

Noninterference for Free
William J. Bowman and Amal Ahmed
(Northeastern University, USA)
Algebras and Coalgebras in the Light Affine Lambda Calculus
Marco Gaboardi and Romain Péchoux
(University of Dundee, UK; University of Lorraine, France)
Structures for Structural Recursion
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola
(University of Oregon, USA)
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)
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)

Keynote 2

Functional Programming and Hardware Design: Still Interesting after All These Years
Mary Sheeran
(Chalmers University of Technology, Sweden)

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)
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)
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)

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

Session 8: Foundations II

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

Session 9: Information Flow

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

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

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

Session 12: Contracts

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

Session 13: Type Checking

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

proc time: 0.7