Links to accepted papers for the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016). Pull requests welcome!

(Similar pages are available for older ICFP (2012, 2013, 2014, 2015), POPL (2013, 2014, 2015, 2016), and PLDI 2014.)

Note: if you are editing this repository, please remember to use the Markdown syntax for hard line breaks, namely two spaces at the end of the line.

ICFP 2016

A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors
Katsuhiro Ueno, Atsushi Ohori
(preprint)

A Glimpse of Hopjs
Manuel Serrano, Vincent Prunet
(preprint from HAL)

A Lambda-Calculus Foundation for Universal Probabilistic Programming
Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak
(preprint from arXiv)

A New Verified Compiler Backend for CakeML
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrsh
(preprint)

A Type Theory for Incremental Computational Complexity with Control Flow Changes
Ezgi Çiçek, Zoe Paraskevopoulou, Deepak Garg
(preprint)

All Sorts of Permutations (Functional Pearl)
Jan Christiansen, Nikita Danilenko, Sandra Dylus
(preprint)

Allocation Characterizes Polyvariance
Thomas Gilray, Michael D. Adams, Matthew Might
(preprint)

An Abstract Memory Functor for Verified C Static Analyzers
Sandrine Blazy, Vincent Laporte, David Pichardie
(draft)

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

Combining Effects and Coeffects via Grading
Marco Gaboardi, Shinya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu
(draft)

Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms
Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara

Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
David Darais, David Van Horn
(preprint)

Dag-Calculus: A Calculus for Parallel Computation
Umut Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski
(preprint)

Datafun: A Functional Datalog
Michael Arntzenius, Neelakantan Krishnaswami
(preprint)

Deriving a Probability Density Calculator (Functional Pearl)
Wazim Mohammed Ismail, Chung-chieh Shan
(preprint)

Disjoint Intersection Types
Bruno Oliveira, Zhiyuan Shi, João Miguel Queiroz de Ataíde Agorreta de Alpuim
(draft)

Dynamic Witnesses for Static Type Errors
Eric Seidel, Ranjit Jhala, Westley Weimer
(draft)

Elaborator Reflection: Extending Idris in Idris
David Christiansen, Edwin Brady
(draft)

Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
Ilya Sergey
(preprint)

Farms, Pipes, Streams, and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms
David Castro, Kevin Hammond, Susmit Sarkar

Fully Abstract Compilation via Universal Embedding
Max New, William J. Bowman, Amal Ahmed
(preprint)

Ghostbuster: A Tool for Simplifying and Converting GADTs
Trevor McDonell, Timothy Zakian, Matteo Cimini, Ryan Newton
(preprint)

Hierarchical Memory Management for Parallel Programs
Ram Raghunathan, Stefan K. Muller, Umut Acar, Guy Blelloch

Higher-Order Ghost State
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
(preprint)

Indexed Codata Types
David Thibodeau, Andrew Cave, Brigitte Pientka
(preprint)

Oh Lord, Please Don't Let Contracts Be Misunderstood: A Variation on Old Gems (Functional Pearl)
Christos Dimoulas, Max New, Robby Findler, Matthias Felleisen
(preprint)

Partial Type Equivalences for Verified Dependent Interoperability
Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter
(preprint)

Queueing and Glueing for Optimal Partitioning (Functional Pearl)
Shin-Cheng Mu, Yu-Hsi Chiang, Yu-Han Lyu
(preprint)

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, Gerwin Klein
(draft, preprint will be available after the conference)

Sequent Calculus as a Compiler Intermediate Language
Paul Downen, Luke Maurer, Zena Ariola, Simon Peyton Jones
(extended version)

Set-Theoretic Types for Polymorphic Variants
Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn
(preprint from arXiv)

String Diagrams for Free Monads (Functional Pearl)
Maciej Piróg, Nicolas Wu
(preprint)

Talking Bananas: Structural Recursion for Session Types
Sam Lindley, J. Garrett Morris
(preprint)

The Best of Both Worlds: Linear Functional Programming without Compromise
J. Garrett Morris
(preprint)

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, Hideya Iwasaki

Context-Free Session Types
Peter Thiemann, Vasco Vasconcelos
(preprint)

Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Jesper Cockx, Dominique Devriese, Frank Piessens
(preprint)

Co-located events

As of writing, the submission process for most ICFP'16 co-located events is not finished. Feel free to send a pull-request with list of accepted papers and contribute links to preprints.

TyDe 2016 (video recordings of the talks)

APLicative Programming with Naperian Functors (Extended Abstract)
Jeremy Gibbons.
(preprint)

Choose Your Own Derivative (Extended Abstract)
Jennifer Paykin, Antal Spector-Zabusky, and Kenneth Foner.
(draft)

An Agda Formalisation of the Transitive Closure of Block Matrices (Extended Abstract)
Adam Sandberg Eriksson and Patrik Jansson.
(talk video, preprint, GitHub source, slides)

Generic diff3 for Algebraic Datatypes
Marco Vassena.
(talk video)

Programming Assistance for Type-Directed Programming (Extended Abstract)
Peter-Michael Osera.

Generic Partially-Static Data (Extended Abstract)
David Kaloper and Jeremy Yallop.
(draft)

Bidirectional Transformations Are Proof-Relevant Bisimulations (Extended Abstract)
James McKinna.

Applications of Applicative Proof Search
Liam O'Connor.

Generic Lookup and Update for Infinitary Inductive-Recursive Types
Larry Diehl and Tim Sheard.
(draft)

Programming with Monadic CSP-Style Processes in Dependent Type Theory
Bashar Igried and Anton Setzer.

Liberating Effects with Rows and Handlers
Daniel Hillerström and Sam Lindley.
(draft)

Parameterized Extensible Effects and Session Types (Extended Abstract)
Oleg Kiselyov.

Haskell Symposium 2016

AUTOBAHN: Using Genetic Algorithms to Infer Strictness Annotations
Y. Wang, D. Nunez, K. Fisher.

Causal commutative arrows revisited
J. Yallop, H. Liu.
(draft)

Desugaring Haskell's do-notation Into Applicative Operations
S. Marlow, S. Jones, E. Kmett, A. Mokhov.
(draft)

Embedding Session Types in Haskell
S. Lindley, J. G. Morris.
(draft)

Experience Report: Developing High Performance HTTP/2 Server in Haskell
K. Yamamoto.

FitSpec: refining property sets for functional testing
R. Braquehais, C. Runciman.

Free Delivery (functional pearl)
J. Gibbons.
(preprint)

Functional Reactive Programming, Refactored
I. Perez, M. Barenz, H. Nilsson.
(draft)

High-performance client-side web applications through Haskell EDSLs
A. Ekblad.
(draft)

How to twist pointers without breaking them
S. Chauhan, P. Kurur, B. Yorgey.
(draft)

The Key Monad:Type-Safe Unconstrained Dynamic Typing
P. Buiras, K. Claessen, A. Ploeg.

Lazy Graph Processing in Haskell
P. Dexter, Y. Liu, K. Chiu.
(draft)

Non-recursive Make Considered Harmful
A. Mokhov, N. Mitchell, S. Peyton Jones, S. Marlow.
(draft)

Pattern Synonyms
M. Pickering, G. Érdi, S. Peyton Jones, R. Eisenberg.
(preprint)

QuickFuzz: an automatic random fuzzer for common file formats
G. Grieco, M. Ceresa, P. Buiras.
(preprint, implementation)

Revisiting Software Transactional Memory in Haskell
M. Le, R. Yates, M. Fluet.
(preprint)

Supermonads - One Notion to Bind Them All
J. Bracker, H. Nilsson.
(preprint)

Types for a Relational Algebra Library (Experience Report)
M. Agren, L. Augustsson.

ML Workshop 2016

WebAssembly: high speed at low cost for everyone
Andreas Rossberg

Extracting from F* to C: a progress report
Jonathan Protzenko, Karthikeyan Bhargavan, Jean-Karim Zinzindohoué, Abhishek Anand, Cédric Fournet, Bryan Parno, Aseem Rastogi and Nikhil Swamy

Compiling with Continuations and LLVM
Kavon Farvardin and John Reppy
(draft)

SML# with Natural Join
Tomohiro Sasaki, Katsuhiro Ueno and Atsushi Ohori

Eff Directly in OCaml
Oleg Kiselyov and Kc Sivaramakrishnan
(draft)

Compiling Links Effect Handlers to the OCaml Backend
Daniel Hillerström, Sam Lindley and Kc Sivaramakrishnan
(draft)

Classes for the Masses
Claudio Russo and Matthew Windsor

Close Encounters of the Higher Kind - Emulating Constructor Classes in Standard ML
Yutaka Nagashima and Liam O'Connor

Malfunctional Programming
Stephen Dolan
(draft)

Ambiguous pattern variables
Gabriel Scherer, Luc Maranget and Thomas Réfis
(draft)

Typed Embedding of Relational Language in OCaml
Dmitri Kosarev and Dmitri Boulytchev
(draft)

FARM 2016

Full Papers

Bithoven: Gödel Encoding of Chamber Music and Functional 8-Bit Audio Synthesis
Jay McCarthy
(preprint)

Juniper: A Functional Reactive Programming Language for the Arduino
Caleb Helbling and Samuel Guyer (preprint, implementation)

Arrp: A Functional Language with Multi-dimensional Signals and Recurrence Equations
Jakob Leben

Structured Reactive Programming with Polymorphic Temporal Tiles
David Janin and Simon Archipoff

o.OM: Structured-Functional Communication between Computer Music Systems using OSC and Odot
Jean Bresson, John MacCallum and Adrian Freed

A Livecoding Semantics for Functional Reactive Programming
Tom E. Murphy

Calls for Collaboration

Call for Collaboration: Algomusicology, ????, Profit
Chris Ford

Demos

Demo: Klangmeister
Chris Ford
(demo page)

Demo: VoxelCAD, a collaborative voxel-based CAD tool
Csongor Kiss and Toby Shaw
(demo page)

Demo: Alda: A text-based music composition language
Dave Yarwood
(demo page)

Demo: Epimorphism
Francis Shuman
(demo page)

FHPC 2016

Icicle: write once, run once
Amos Robinson, Ben Lippmeier
(preprint)

Using Fusion to Enable Late Design Decisions for Pipelined Computations
Mate Karacsony, Koen Claessen

Automatic generation of efficient codes from mathematical descriptions of stencil computation
Takayuki Muranushi, Seiya Nishizawa, Hirofumi Tomita, Keigo Nitadori, Masaki Iwasawa, Yutaka Maruyama, Hisashi Yashiro, Yoshifumi Nakamura, Hideyuki Hotta, Junichiro Makino, Natsuki Hosono, Hikaru Inoue

JIT Costing Adaptive Skeletons for Performance Portability
Patrick Maier, John Magnus Morton, Phil Trinder

Low-level functional GPU programming for parallel algorithms
Martin Dybdal, Martin Elsman, Bo Joel Svensson, Mary Sheeran

APL on GPUs - A TAIL from the Past, Scribbled in Futhark
Troels Henriksen, Martin Dybdal, Henrik Urms, Anna Sofie Kiehn , Daniel Gavin , Hjalte Abelskov, Martin Elsman, Cosmin Oancea
(preprint)

Streaming Nested Data Parallelism on Multicores
Frederik Meisner Madsen, Andrzej Filinski

Polarised Data Parallel Data Flow
Ben Lippmeier, Fil Mackay, Amos Robinson
(preprint)

s6raph: Vertex-centric Graph Processing Framework with Functional Interface
Onofre Coll Ruiz, Kiminori Matsuzaki, Shigeyuki Sato

OCaml 2016

Conex - establishing trust into data repositories
Hannes Mehnert and Louis Gesbert
(extended abstract)

Generic Programming in OCaml
Florent Balestrieri and Michel Mauny

Improving the OCaml Web Stack: Motivations and Progress
Spiridon Eliopoulos

Learn OCaml: An Online Learning Center for OCaml
Benjamin Canou, Grégoire Henry, Çagdas Bozman and Fabrice Le Fessant
(extended abstract)

Lock-free programming for the masses
Kc Sivaramakrishnan and Theo Laurent
(extended abstract)

OCaml inside: a drop-in replacement for libtls
Enguerrand Decorne, Jeremy Yallop and David Kaloper Meršinjak
(extended abstract, implementation)

OPAM-builder: Continuous Monitoring of OPAM Repositories
Fabrice Le Fessant
(extended abstract, implementation, build results)

Semantics of the Lambda intermediate language
Pierre Chambart

Statistically profiling memory in OCaml
Jacques-Henri Jourdan
(implementation (ocaml branch))

Sundials/ML: interfacing with numerical solvers
Timothy Bourke, Jun Inoue, Marc Pouzet
(implementation, documentation)

The State of the OCaml Platform: September 2016
Louis Gesbert, on behalf of the OCaml Platform team
(extended abstract)

Who's got your Mail? Mr. Mime!
Romain Calascibetta
(extended abstract, implementation)

The following works will be presented as posters during a dedicated poster session:

Inuit library: from printf to interactive user-interfaces
Frédéric Bour

ocp-lint, A Plugin-based Style-Checker with Semantic Patches
Çagdas Bozman, Théophane Hufschmitt, Michael Laporte and Fabrice Le Fessant
(extended abstract, implementation)

Partial evaluation and metaprogramming
Pierre Chambart

Scheme 2016

Ghosts in the machine
Daniel Szmulewicz

A Scheme concurrency library
Takashi Kato

Nash: a tracing JIT for extension language
Atsuro Hoshino

Function compose, Type cut, And the Algebra of logic
XIE Yuheng

Multi-purpose web framework design based on websocket over HTTP Gateway
Mu Lei

Deriving Pure, Functional One-Pass Operations for Processing Tail-Aligned Lists
Jason Hemann, Daniel P. Friedman

miniAdapton: A Minimal Implementation of Incremental Computation in Scheme
Dakota Fisher, Matthew Hammer, William Byrd, Matthew Might