ICFP 2016
21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)
Powered by
Conference Publishing Consulting

21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), September 18–24, 2016, Nara, Japan

ICFP 2016 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Message from the Chairs
ICFP 2016 Organization
Sponsors

Invited Talks

TensorFlow: Learning Functions at Scale
Martín Abadi
(Google, USA)
Publisher's Version Article Search
Journey to Find Bugs in JavaScript Web Applications in the Wild
Sukyoung Ryu
(KAIST, South Korea)
Publisher's Version Article Search
A Functional Programmer's Guide to Homotopy Type Theory
Dan Licata
(Wesleyan University, USA)
Publisher's Version Article Search

Research Track

Session 1

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)
Publisher's Version Article Search
Dag-Calculus: A Calculus for Parallel Computation
Umut A. Acar, Arthur Charguéraud, Mike Rainey, and Filip Sieczkowski
(Carnegie Mellon University, USA; Inria, France)
Publisher's Version Article Search
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)
Publisher's Version Article Search
Deriving a Probability Density Calculator (Functional Pearl)
Wazim Mohammed Ismail and Chung-chieh Shan
(Indiana University, USA)
Publisher's Version Article Search

Session 2

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

Session 3

Fully Abstract Compilation via Universal Embedding
Max S. New, William J. Bowman, and Amal Ahmed
(Northeastern University, USA)
Publisher's Version Article Search 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)
Publisher's Version Article Search
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)
Publisher's Version Article Search

Session 4

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)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info
All Sorts of Permutations (Functional Pearl)
Jan Christiansen, Nikita Danilenko, and Sandra Dylus
(Flensburg University of Applied Sciences, Germany; University of Kiel, Germany)
Publisher's Version Article Search

Session 5

A Glimpse of Hopjs
Manuel Serrano and Vincent Prunet
(Inria, France)
Publisher's Version Article Search Info
Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
Ilya Sergey
(University College London, UK)
Publisher's Version Article Search 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)
Publisher's Version Article Search
Datafun: A Functional Datalog
Michael Arntzenius and Neelakantan R. Krishnaswami
(University of Birmingham, UK)
Publisher's Version Article Search

Session 6

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)
Publisher's Version Article Search
Automatically Disproving Fair Termination of Higher-Order Functional Programs
Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, and Naoki Kobayashi
(University of Tokyo, Japan)
Publisher's Version Article Search
Higher-Order Ghost State
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer
(MPI-SWS, Germany; Aarhus University, Denmark)
Publisher's Version Article Search Info

Session 7

Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Jesper Cockx, Dominique Devriese, and Frank Piessens
(iMinds, Belgium; KU Leuven, Belgium)
Publisher's Version Article Search
Elaborator Reflection: Extending Idris in Idris
David Christiansen and Edwin Brady
(Indiana University, USA; University of St. Andrews, UK)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info

Session 8

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais and David Van Horn
(University of Maryland, USA)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info

Session 9

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)
Publisher's Version Article Search Artifacts Available
Indexed Codata Types
David Thibodeau, Andrew Cave, and Brigitte Pientka
(McGill University, Canada)
Publisher's Version Article Search
Disjoint Intersection Types
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim
(University of Hong Kong, China)
Publisher's Version Article Search
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)
Publisher's Version Article Search Info

Session 10

Hierarchical Memory Management for Parallel Programs
Ram Raghunathan, Stefan K. Muller, Umut A. Acar, and Guy Blelloch
(Carnegie Mellon University, USA; Inria, France)
Publisher's Version Article Search
Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-Flow Analysis
Thomas Gilray, Michael D. Adams, and Matthew Might
(University of Utah, USA)
Publisher's Version Article Search
A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors
Katsuhiro Ueno and Atsushi Ohori
(Tohoku University, Japan)
Publisher's Version Article Search

Session 11

Talking Bananas: Structural Recursion for Session Types
Sam Lindley and J. Garrett Morris
(University of Edinburgh, UK)
Publisher's Version Article Search
The Best of Both Worlds: Linear Functional Programming without Compromise
J. Garrett Morris
(University of Edinburgh, UK)
Publisher's Version Article Search
Context-Free Session Types
Peter Thiemann and Vasco T. Vasconcelos
(University of Freiburg, Germany; University of Lisbon, Portugal)
Publisher's Version Article Search

Session 12

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)
Publisher's Version Article Search
String Diagrams for Free Monads (Functional Pearl)
Maciej Piróg and Nicolas Wu
(KU Leuven, Belgium; University of Bristol, UK)
Publisher's Version Article Search

proc time: 0.3