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 RyuORCID logo
(KAIST, South Korea)
A Functional Programmer's Guide to Homotopy Type Theory
Dan Licata ORCID logo
(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 ORCID logo, Arthur CharguéraudORCID logo, Mike Rainey, and Filip Sieczkowski
(Carnegie Mellon University, USA; Inria, France)
A Lambda-Calculus Foundation for Universal Probabilistic Programming
Johannes Borgström, Ugo Dal LagoORCID logo, 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 ORCID logo
(Indiana University, USA)

Session 2

A New Verified Compiler Backend for CakeML
Yong Kiam Tan, Magnus O. MyreenORCID logo, Ramana Kumar, Anthony Fox, Scott Owens ORCID logo, and Michael Norrish ORCID logo
(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 DownenORCID logo, 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

Session 3

Fully Abstract Compilation via Universal Embedding
Max S. New, William J. Bowman ORCID logo, and Amal AhmedORCID logo
(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 ORCID logo
(PLT, USA)
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Ezgi Çiçek, Zoe Paraskevopoulou, and Deepak GargORCID logo
(MPI-SWS, Germany; Princeton University, USA)

Session 4

Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms
Kotaro Takeda, Naoki KobayashiORCID logo, 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)

Session 5

A Glimpse of Hopjs
Manuel SerranoORCID logo 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 MorihataORCID logo, and Hideya Iwasaki ORCID logo
(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 ORCID logo, and Naoki KobayashiORCID logo
(University of Tokyo, Japan)
Higher-Order Ghost State
Ralf JungORCID logo, Robbert Krebbers, Lars BirkedalORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; Aarhus University, Denmark)
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)
Elaborator Reflection: Extending Idris in Idris
David Christiansen and Edwin BradyORCID logo
(Indiana University, USA; University of St. Andrews, UK)
Partial Type Equivalences for Verified Dependent Interoperability
Pierre-Evariste Dagand, Nicolas TabareauORCID logo, and Éric TanterORCID logo
(UPMC, France; LIP6, France; Inria, France; University of Chile, Chile)
Info

Session 8

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais and David Van HornORCID logo
(University of Maryland, USA)
An Abstract Memory Functor for Verified C Static Analyzers
Sandrine Blazy ORCID logo, Vincent Laporte, and David Pichardie ORCID logo
(University of Rennes 1, France; IRISA, France; IMDEA Software Institute, Spain; ENS Rennes, France)
Info

Session 9

Ghostbuster: A Tool for Simplifying and Converting GADTs
Trevor L. McDonell ORCID logo, 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 PientkaORCID logo
(McGill University, Canada)
Disjoint Intersection Types
Bruno C. d. S. OliveiraORCID logo, 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

Session 10

Hierarchical Memory Management for Parallel Programs
Ram Raghunathan, Stefan K. Muller, Umut A. Acar ORCID logo, 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 ORCID logo 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 ThiemannORCID logo and Vasco T. VasconcelosORCID logo
(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.78