ICFP 2016
21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)

Title Page

Message from the Chairs

ICFP 2016 Organization

Sponsors

TensorFlow: Learning Functions at Scale
Martín Abadi
(Google, USA)

Journey to Find Bugs in JavaScript Web Applications in the Wild
Sukyoung Ryu
(KAIST, South Korea)

A Functional Programmer's Guide to Homotopy Type Theory
Dan Licata
(Wesleyan University, USA)

Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms
David Castro, Kevin Hammond, and Susmit Sarkar
(University of St. Andrews, UK)

Dag-Calculus: A Calculus for Parallel Computation
Umut A. Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski
(Carnegie Mellon University, USA; Inria, France)

A Lambda-Calculus Foundation for Universal Probabilistic Programming
Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak
(Uppsala University, Sweden; University of Bologna, Italy; Inria, France; Microsoft Research, UK; University of Edinburgh, UK)

Deriving a Probability Density Calculator (Functional Pearl)
Wazim Mohammed Ismail and Chung-chieh Shan
(Indiana University, USA)

A New Verified Compiler Backend for CakeML
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish
(IHPC at A*STAR, Singapore; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia; UNSW, Australia; University of Cambridge, UK; University of Kent, UK; Australian National University, Australia)

Sequent Calculus as a Compiler Intermediate Language
Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyton Jones
(University of Oregon, USA; Microsoft Research, UK)

Info

Refinement through Restraint: Bringing Down the Cost of Verification
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein
(UNSW, Australia; Data61, Australia; University of Pennsylvania, USA; University of Melbourne, Australia)

Info

Fully Abstract Compilation via Universal Embedding
Max S. New, William J. Bowman, and Amal Ahmed
(Northeastern University, USA)

Info

Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Christos Dimoulas, Max S. New, Robert Bruce Findler, and Matthias Felleisen
(PLT, USA)

A Type Theory for Incremental Computational Complexity with Control Flow Changes
Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak Garg
(MPI-SWS, Germany; Princeton University, USA)

Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms
Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, and Ayumi Shinohara
(University of Tokyo, Japan; Tohoku University, Japan)

Queueing and Glueing for Optimal Partitioning (Functional Pearl)
Shin-Cheng Mu, Yu-Hsi Chiang, and Yu-Han Lyu
(Academia Sinica, Taiwan; National Taiwan University, Taiwan; Dartmouth College, USA)

Info

All Sorts of Permutations (Functional Pearl)
Jan Christiansen, Nikita Danilenko, and Sandra Dylus
(Flensburg University of Applied Sciences, Germany; University of Kiel, Germany)

A Glimpse of Hopjs
Manuel Serrano and Vincent Prunet
(Inria, France)

Info

Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
Ilya Sergey
(University College London, UK)

Info

Think Like a Vertex, Behave Like a Function! A Functional DSL for Vertex-Centric Big Graph Processing
Kento Emoto, Kiminori Matsuzaki, Zhenjiang Hu, Akimasa Morihata, and Hideya Iwasaki
(Kyushu Institute of Technology, Japan; Kochi University of Technology, Japan; National Institute of Informatics, Japan; University of Tokyo, Japan; University of Electro-Communications, Japan)

Datafun: A Functional Datalog
Michael Arntzenius and Neelakantan R. Krishnaswami
(University of Birmingham, UK)

Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
Eric L. Seidel, Ranjit Jhala, and Westley Weimer
(University of California at San Diego, USA; University of Virginia, USA)

Automatically Disproving Fair Termination of Higher-Order Functional Programs
Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, and Naoki Kobayashi
(University of Tokyo, Japan)

Higher-Order Ghost State
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer
(MPI-SWS, Germany; Aarhus University, Denmark)

Info

Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Jesper Cockx, Dominique Devriese, and Frank Piessens
(iMinds, Belgium; KU Leuven, Belgium)

Elaborator Reflection: Extending Idris in Idris
David Christiansen and Edwin Brady
(Indiana University, USA; University of St. Andrews, UK)

Partial Type Equivalences for Verified Dependent Interoperability
Pierre-Evariste Dagand, Nicolas Tabareau, and Éric Tanter
(UPMC, France; LIP6, France; Inria, France; University of Chile, Chile)

Info

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais and David Van Horn
(University of Maryland, USA)

An Abstract Memory Functor for Verified C Static Analyzers
Sandrine Blazy, Vincent Laporte, and David Pichardie
(University of Rennes 1, France; IRISA, France; IMDEA Software Institute, Spain; ENS Rennes, France)

Info

Ghostbuster: A Tool for Simplifying and Converting GADTs
Trevor L. McDonell, Timothy A. K. Zakian, Matteo Cimini, and Ryan R. Newton
(Indiana University, USA; Oxford University, UK)

Indexed Codata Types
David Thibodeau, Andrew Cave, and Brigitte Pientka
(McGill University, Canada)

Disjoint Intersection Types
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim
(University of Hong Kong, China)

Set-Theoretic Types for Polymorphic Variants
Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn
(University of Paris Diderot, France; University of Genoa, Italy; University of Paris-Sud, France)

Info

Hierarchical Memory Management for Parallel Programs
Ram Raghunathan, Stefan K. Muller, Umut A. Acar, and Guy Blelloch
(Carnegie Mellon University, USA; Inria, France)

Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-Flow Analysis
Thomas Gilray, Michael D. Adams, and Matthew Might
(University of Utah, USA)

A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors
Katsuhiro Ueno and Atsushi Ohori
(Tohoku University, Japan)

Talking Bananas: Structural Recursion for Session Types
Sam Lindley and J. Garrett Morris
(University of Edinburgh, UK)

The Best of Both Worlds: Linear Functional Programming without Compromise
J. Garrett Morris
(University of Edinburgh, UK)

Context-Free Session Types
Peter Thiemann and Vasco T. Vasconcelos
(University of Freiburg, Germany; University of Lisbon, Portugal)

Combining Effects and Coeffects via Grading
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu
(SUNY Buffalo, USA; Kyoto University, Japan; University of Cambridge, UK; University of Kent, UK; Inria, France; Tallinn University of Technology, Estonia)

String Diagrams for Free Monads (Functional Pearl)
Maciej Piróg and Nicolas Wu
(KU Leuven, Belgium; University of Bristol, UK)