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
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
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
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, Sidney Amani, Christine Rizkallah, Japheth Lim, Thomas Sewll, Yutaka Nagashima, Alex Hixon, Joseph Tuong, Toby Murray, Gerwin Klein, Gernot Heiser
(draft)
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
Towards Context-Free Session Types
Peter Thiemann, Vasco Vasconcelos
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
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 P. Jansson.
(preprint, GitHub source)
Generic diff3 for Algebraic Datatypes
Marco Vassena.
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
J. Bracker, H. Nilsson.
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
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
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
(draft)
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
(draft)
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