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

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

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

Session 3

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

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

Session 5

A Glimpse of Hopjs
Manuel Serrano and Vincent Prunet
(Inria, France)
Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
Ilya Sergey
(University College London, UK)
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)

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

Session 7

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)

Session 8

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)

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

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

Session 11

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)

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

proc time: 0.7