Frontmatter

Keynote 1

Program Synthesis: Opportunities for the Next Decade
Rastislav Bodik
(University of Washington, USA)


@InProceedings{ICFP15p1, author = {Rastislav Bodik}, title = {Program Synthesis: Opportunities for the Next Decade}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {1-0}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p15, author = {Tiark Rompf and Nada Amin}, title = {Functional Pearl: A SQL to C Compiler in 500 Lines of Code}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {15-14}, doi = {}, year = {2015}, }

An Optimizing Compiler for a Purely Functional Web-Application Language
Adam Chlipala
(Massachusetts Institute of Technology, USA)


@InProceedings{ICFP15p29, author = {Adam Chlipala}, title = {An Optimizing Compiler for a Purely Functional Web-Application Language}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {29-28}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p43, author = {Spenser Bauman and Carl Friedrich Bolz and Robert Hirschfeld and Vasily Kirilichev and Tobias Pape and Jeremy G. Siek and Sam Tobin-Hochstadt}, title = {Pycket: A Tracing JIT for a Functional Language}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {43-42}, doi = {}, year = {2015}, }

Session 2: Types

1ML – Core and Modules United (F-ing First-Class Modules)
Andreas Rossberg
(Google, Germany)


@InProceedings{ICFP15p57, author = {Andreas Rossberg}, title = {1ML – Core and Modules United (F-ing First-Class Modules)}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {57-56}, doi = {}, year = {2015}, }

Bounded Refinement Types
Niki Vazou, Alexander Bakst, and Ranjit Jhala
(University of California at San Diego, USA)


@InProceedings{ICFP15p71, author = {Niki Vazou and Alexander Bakst and Ranjit Jhala}, title = {Bounded Refinement Types}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {71-70}, doi = {}, year = {2015}, }

Session 3: Miscellaneous

Applicative Bidirectional Programming with Lenses
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Kent, UK)


@InProceedings{ICFP15p85, author = {Kazutaka Matsuda and Meng Wang}, title = {Applicative Bidirectional Programming with Lenses}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {85-84}, doi = {}, year = {2015}, }

Hygienic Resugaring of Compositional Desugaring
Justin Pombrio and Shriram Krishnamurthi
(Brown University, USA)


@InProceedings{ICFP15p99, author = {Justin Pombrio and Shriram Krishnamurthi}, title = {Hygienic Resugaring of Compositional Desugaring}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {99-98}, doi = {}, year = {2015}, }

XQuery and Static Typing: Tackling the Problem of Backward Axes
Pierre Genevès and Nils Gesbert
(University of Grenoble, France; CNRS, France; INRIA, France)


@InProceedings{ICFP15p113, author = {Pierre Genevès and Nils Gesbert}, title = {XQuery and Static Typing: Tackling the Problem of Backward Axes}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {113-112}, doi = {}, year = {2015}, }

Session 4: Foundations I

Noninterference for Free
William J. Bowman and Amal Ahmed
(Northeastern University, USA)


@InProceedings{ICFP15p127, author = {William J. Bowman and Amal Ahmed}, title = {Noninterference for Free}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {127-126}, doi = {}, year = {2015}, }

Algebras and Coalgebras in the Light Affine Lambda Calculus
Marco Gaboardi and Romain Péchoux
(University of Dundee, UK; University of Lorraine, France)


@InProceedings{ICFP15p141, author = {Marco Gaboardi and Romain Péchoux}, title = {Algebras and Coalgebras in the Light Affine Lambda Calculus}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {141-140}, doi = {}, year = {2015}, }

Structures for Structural Recursion
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola
(University of Oregon, USA)


@InProceedings{ICFP15p155, author = {Paul Downen and Philip Johnson-Freyd and Zena M. Ariola}, title = {Structures for Structural Recursion}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {155-154}, doi = {}, year = {2015}, }

Session 5: Cost Analysis

Denotational Cost Semantics for Functional Languages with Inductive Types
Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa
(Wesleyan University, USA)


@InProceedings{ICFP15p169, author = {Norman Danner and Daniel R. Licata and Ramyaa Ramyaa}, title = {Denotational Cost Semantics for Functional Languages with Inductive Types}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {169-168}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p183, author = {Martin Avanzini and Ugo Dal Lago and Georg Moser}, title = {Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {183-182}, doi = {}, year = {2015}, }

Keynote 2

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


@InProceedings{ICFP15p197, author = {Mary Sheeran}, title = {Functional Programming and Hardware Design: Still Interesting after All These Years}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {197-196}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p211, author = {Georg Neis and Chung-Kil Hur and Jan-Oliver Kaiser and Craig McLaughlin and Derek Dreyer and Viktor Vafeiadis}, title = {Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {211-210}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p225, author = {Beta Ziliani and Matthieu Sozeau}, title = {A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {225-224}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p239, author = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel}, title = {Foundational Extensible Corecursion: A Proof Assistant Perspective}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {239-238}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p253, author = {Michel Steuwer and Christian Fensch and Sam Lindley and Christophe Dubach}, title = {Generating Performance Portable Code using Rewrite Rules: From High-Level Functional Expressions to High-Performance OpenCL Code}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {253-252}, doi = {}, year = {2015}, }

Adaptive Lock-Free Maps: Purely-Functional to Scalable
Ryan R. Newton, Peter P. Fogg, and Ali Varamesh
(Indiana University, USA)


@InProceedings{ICFP15p267, author = {Ryan R. Newton and Peter P. Fogg and Ali Varamesh}, title = {Adaptive Lock-Free Maps: Purely-Functional to Scalable}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {267-266}, doi = {}, year = {2015}, }

Partial Aborts for Transactions via First-Class Continuations
Matthew Le and Matthew Fluet
(Rochester Institute of Technology, USA)


@InProceedings{ICFP15p281, author = {Matthew Le and Matthew Fluet}, title = {Partial Aborts for Transactions via First-Class Continuations}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {281-280}, doi = {}, year = {2015}, }

Session 8: Foundations II

Which Simple Types Have a Unique Inhabitant?
Gabriel Scherer and Didier Rémy
(INRIA, France)


@InProceedings{ICFP15p295, author = {Gabriel Scherer and Didier Rémy}, title = {Which Simple Types Have a Unique Inhabitant?}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {295-294}, doi = {}, year = {2015}, }

Elaborating Evaluation-Order Polymorphism
Joshua Dunfield
(University of British Columbia, Canada)


@InProceedings{ICFP15p309, author = {Joshua Dunfield}, title = {Elaborating Evaluation-Order Polymorphism}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {309-308}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p323, author = {Tillmann Rendel and Julia Trieflinger and Klaus Ostermann}, title = {Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {323-322}, doi = {}, year = {2015}, }

Session 9: Information Flow

Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell
Alejandro Russo
(Chalmers University of Technology, Sweden)


@InProceedings{ICFP15p337, author = {Alejandro Russo}, title = {Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {337-336}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p351, author = {Pablo Buiras and Dimitrios Vytiniotis and Alejandro Russo}, title = {HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {351-350}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p365, author = {Atze van der Ploeg and Koen Claessen}, title = {Practical Principled FRP: Forget the Past, Change the Future, FRPNow!}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {365-364}, doi = {}, year = {2015}, }

Certified Symbolic Management of Financial Multi-party Contracts
Patrick Bahr, Jost Berthold, and Martin Elsman
(University of Copenhagen, Denmark; Commonwealth Bank of Australia, Australia)


@InProceedings{ICFP15p379, author = {Patrick Bahr and Jost Berthold and Martin Elsman}, title = {Certified Symbolic Management of Financial Multi-party Contracts}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {379-378}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p393, author = {Steffen Smolka and Spiridon Eliopoulos and Nate Foster and Arjun Guha}, title = {A Fast Compiler for NetKAT}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {393-392}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p407, author = {Nicolas Stucki and Tiark Rompf and Vlad Ureche and Phil Bagwell}, title = {RRB Vector: A Practical General Purpose Immutable Sequence}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {407-406}, doi = {}, year = {2015}, }

Functional Pearl: A Smart View on Datatypes
Mauro Jaskelioff and Exequiel Rivas
(CIFASIS-CONICET, Argentina; Universidad Nacional de Rosario, Argentina)


@InProceedings{ICFP15p421, author = {Mauro Jaskelioff and Exequiel Rivas}, title = {Functional Pearl: A Smart View on Datatypes}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {421-420}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p435, author = {Edward Z. Yang and Giovanni Campagna and Ömer S. Ağacan and Ahmed El-Hassany and Abhishek Kulkarni and Ryan R. Newton}, title = {Efficient Communication and Collection with Compact Normal Forms}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {435-434}, doi = {}, year = {2015}, }

Session 12: Contracts

Blame Assignment for Higher-Order Contracts with Intersection and Union
Matthias Keil and Peter Thiemann
(University of Freiburg, Germany)


@InProceedings{ICFP15p449, author = {Matthias Keil and Peter Thiemann}, title = {Blame Assignment for Higher-Order Contracts with Intersection and Union}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {449-448}, doi = {}, year = {2015}, }

Expressing Contract Monitors as Patterns of Communication
Cameron Swords, Amr Sabry, and Sam Tobin-Hochstadt
(Indiana University, USA)


@InProceedings{ICFP15p463, author = {Cameron Swords and Amr Sabry and Sam Tobin-Hochstadt}, title = {Expressing Contract Monitors as Patterns of Communication}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {463-462}, doi = {}, year = {2015}, }

Learning Refinement Types
He Zhu, Aditya V. Nori, and Suresh Jagannathan
(Purdue University, USA; Microsoft Research, USA)


@InProceedings{ICFP15p477, author = {He Zhu and Aditya V. Nori and Suresh Jagannathan}, title = {Learning Refinement Types}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {477-476}, doi = {}, year = {2015}, }

Session 13: Type Checking

Practical SMT-Based Type Error Localization
Zvonimir Pavlinovic, Tim King, and Thomas Wies
(New York University, USA; VERIMAG, France)


@InProceedings{ICFP15p491, author = {Zvonimir Pavlinovic and Tim King and Thomas Wies}, title = {Practical SMT-Based Type Error Localization}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {491-490}, doi = {}, year = {2015}, }

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)


@InProceedings{ICFP15p505, author = {Georgios Karachalias and Tom Schrijvers and Dimitrios Vytiniotis and Simon Peyton Jones}, title = {GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness}, booktitle = {Proc.\ ICFP}, publisher = {ACM}, pages = {505-504}, doi = {}, year = {2015}, }

proc time: 0.69