Links to conditionally¹ accepted papers for the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP 2017). Pull requests welcome!

(Similar pages are available for older ICFP (2012, 2013, 2014, 2015, 2016), 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.

¹: This year is the first year where ICFP uses a journal publication model, with open-access proceedings published in PACM. A two-phase reviewing process is used, so most papers are conditionally accepted with a list of mandatory revisions for authors to perform.

ICFP 2017

A Framework for Adaptive Differential Privacy
Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, Benjamin C. Pierce
(paper (extended version), video at 23')

A Relational Logic for Higher-Order Programs
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
(preprint from arXiv, video at 27')

A Specification for Dependently-Typed Haskell
Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, Richard Eisenberg
(draft, video at start)

Automating Sized-Type Inference for Complexity Analysis
Martin Avanzini, Ugo Dal Lago
(preprint from arXiv, video at 23')

Better Living Through Operational Semantics: An Optimizing Compiler for Radio Protocols
Geoffrey Mainland
(preprint)

Chaperone Contracts for Higher-Order Sessions
Hernan Melgratti, Luca Padovani
(slides, video at start)

Compiling to categories
Conal Elliott
(preprint, website, video at start)

Constrained Type Families
J. Garrett Morris, Richard Eisenberg
(preprint, video at start)

Definitional Abstract Interpreters for Higher-Order Programming Languages
David Darais, Nicholas Labich, Phúc Nguyễn, David Van Horn
(preprint(https://plum-umd.github.io/abstracting-definitional-interpreters/main.pdf), paper as a webpage!)

Effect-Driven QuickChecking of Compilers
Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson
(preprint, implementation)

Experience Report: Prototyping a Query Compiler Using Coq
Joshua Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jerome Simeon
(video first video)

Faster Coroutine Pipelines
Mike Spivey
(preprint, video at 1')

Foundations of Strong Call by Need
Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, Delia Kesner

Functional Pearl: A Unified Approach to Solving Seven Programming Problems
William E. Byrd, Michael Ballantyne, Greg Rosenblatt, Matthew Might
(video at 1h11')

Functional Pearl: a pretty but not greedy printer
Jean-Philippe Bernardy
(preprint, github repo, video at 26')

Generic functional parallel algorithms: Scan and FFT
Conal Elliott
(preprint, website video at 48'30'')

Gradual Session Types
Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, Philip Wadler
(preprint, slides, video at 1h10')

Gradual Typing with Union and Intersection Types
Giuseppe Castagna, Victor Lanvin
(preprint, video at 52')

Herbarium Racketensis: A Stroll Through the Woods (Functional Pearl)
Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Robby Findler
(paper, video)

How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation
Makoto Hamana
(video)

Imperative functional programs that explain their work
Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney
(preprint from arXiv, companion code)

Inferring Scope through Syntactic Sugar
Justin Pombrio, Shriram Krishnamurthi, Mitchell Wand
(paper, extended version, material, video at 47')

Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind
(preprint, website, video at 2')

Local Refinement Typing
Benjamin Cosman, Ranjit Jhala
(preprint from arXiv, video at 50')

Lock-step simulation is child’s play
Joachim Breitner, Chris Smith
(preprint from arXiv, video at 50'45)

Manifest Sharing with Session Types
Stephanie Balzer, Frank Pfenning
(preprint, video at 47')

A Metaprogramming Framework for Formal Verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
(preprint)

No-brainer CPS Conversion
Milo Davis, William Meehan, Olin Shivers
(video at 1h14')

Normalization by Evaluation for Sized Dependent Types
Andreas Abel, Andrea Vezzosi, Theo Winterhalter
(preprint)

On Polymorphic Gradual Typing
Yuu Igarashi, Taro Sekiyama, Atsushi Igarashi
(preprint, video at 28')

On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
(preprint from arXiv)

Parametric Quantifiers for Dependent Type Theory
Andreas Nuyts, Andrea Vezzosi, Dominique Devriese
(preprint, video at 26')

Persistence for the masses: RRB-Vectors in a systems language
Juan Pedro Bolívar Puente
(preprint, website, github, cppnow17 talk, video at 3')

Scaling up Functional Programming Education: under the hood of the OCaml MOOC
Benjamin Canou, Roberto Di Cosmo, Grégoire Henry
(video at 1h13')

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
(technical report, video at 27'20'')

Staged Generic Programming
Jeremy Yallop
(draft, video at 45')

Super 8, the Story of Making Movies—A Functional Pearl
Leif Andersen, Stephen Chang, Asumu Takikawa, Matthias Felleisen
(preprint)

Symbolic conditioning of arrays in probabilistic programs
Praveen Narayanan, Chung-chieh Shan
(paper, video at 46')

Testing and Debugging Functional Reactive Programming
Ivan Perez, Henrik Nilsson

Theorems for Free for Free: Parametricity, With and Without Types
Amal Ahmed, Dustin Jamner, Jeremy Siek, Philip Wadler
(artifact, video at 4')

Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
(preprint from arXiv, video at 25')

Verifying Efficient Function Calls in CakeML
Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan
(video at 49')

Visitors Unchained
François Pottier
(preprint, video at 23'30'')

Whip: Higher-Order Contracts for Modern Services
Lucas Waye, Christos Dimoulas, Stephen Chong
(preprint from paper webpage, language website, video at 24')

Co-located events

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

Haskell Symposium 2017

Algebraic Programming

Algebraic Graphs with Class (Functional Pearl)
Andrey Mokhov
(draft, hackage)

Back to the Future: Time Travel in FRP
Ivan Perez

Packrats Parse in Packs
Mario Blažević and Jacques Légaré
(pdf, hackage)

Randomness and Testing

Ode on a Random Urn (Functional Pearl)
Leonidas Lampropoulos, Antal Spector-Zabusky, and Kenneth Foner
(pdf)

QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)
Maximilian Algehed, Koen Claessen, Moa Johansson, and Nicholas Smallbone

Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results
Rudy Braquehais and Colin Runciman
(pdf)

Verification

Using Coq to Write Fast and Correct Haskell
John Wiegley and Ben Delaware
(abstract)

A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow
(preprint)

Well-Typed Music Does Not Sound Wrong (Experience Report)
Dmitrij Szamozvancev and Michael Gale

Expressive Types

The Linearity Monad
Jennifer Paykin and Steve Zdancewic
(draft)

Elaboration on Functional Dependencies
Georgios Karachalias and Tom Schrijvers
(draft)

Quantified Class Constraints
Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. D. S. Oliveira, and Philip Wadler
(draft)

Haskell and the Real World

Composable Network Stacks and Remote Monads
Justin Dawson, Mark Grebe, and Andy Gill

A Meta-EDSL for Distributed Web Applications
Anton Ekblad

Hardware Software Co-Design in Haskell
Markus Aronsson and Mary Sheeran

Concurrency and Parallelism

Streaming Irregular Arrays
Robert Clifton-Everest, Trevor L. McDonell, Manuel M T Chakravarty, and Gabriele Keller
(preprint)

Improving STM Performance with Transactional Structs
Ryan Yates and Michael Scott

Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
Chao-Hong Chen, Vikraman Choudhury, and Ryan Newton

FHPC 2017 Workshop on Functional High-Performance Computing

Destination-Passing Style for Efficient Memory Management
Amir Shaikhha, Andrew Fitzgibbon, Simon Peyton Jones, Dimitrios Vytiniotis (preprint)

From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation
Geoffrey Mainland, Siddhanathan Shanmugam

In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions
Adam Barwell, Kevin Hammond
(video at 1h12')

Strategies for Regular Segmented Reductions on GPU
Rasmus Wriedt Larsen, Troels Henriksen

VisPar: Visualising dataflow graphs from the Par monad
Maximilian Algehed, Patrik Jansson
(postprint, VisPar source)

Higher-Order Programming with Effects (HOPE) 2017

A monadic solution to the Cartwright-Felleisen-Wadler conjecture
Ohad Kammar, Dylan McDermott
(preprint from arXiv)

Handling fibred algebraic effects
Danel Ahman
(paper)

Higher-order Programming is an Effect
Oleg Kiselyov

Invited Talk: Semantics of Effect Systems by Graded Monads
Shin-ya Katsumata

Logical Relations for Algebraic Effects
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski

Only Control Effects and Dependent Types
Youyou Cong, William J. Bowman

Recalling a Witness
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy, Cédric Fournet
(preprint from arXiv)

RustBelt: Securing the Foundations of the Rust Programming Language
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
(paper)

Structured Asynchrony with Algebraic Effects
Daan Leijen
(technical report)

ML Family Workshop

Effects without monads: non-determinism.
Oleg Kiselyov

Tierless modules
Gabriel Radanne and Jérôme Vouillon
(extended abstract) (technical report)

Efficient representation of large, dynamic sequences in ML
Arthur Chargueraud and Mike Rainey

Mergeable types
Gowtham Kaki, KC Sivaramakrishnan, Samodya Abeysiriwardane, and Suresh Jagannathan
(draft)

Towards abductive functional programming
Koko Muroya

Typer: an infix statically typed Lisp
Pierre Delaunay, Vincent Archambault-Bouffard, and Stefan Monnier

Making SML# a general-purpose high-performance language
Atsushi Ohori, Kenjiro Taura, and Katsuhiro Ueno
(draft)

First-class subtypes
Jeremy Yallop and Stephen Dolan
(draft)

Effectively tackling the awkward squad
Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, KC Sivaramakrishnan, and Leo White
(draft)

Relational conversion for OCaml
Petr Lozov and Dmitry Boulytchev

VOCAL -- A Verified OCAml Library
Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, François Pottier
(extended abstract)

OCaml Workshop 2017

A B-tree library for OCaml
Tom Ridge
(extended abstract; draft slides)

A memory model for multicore OCaml
Stephen Dolan, KC Sivaramakrishnan
(extended abstract)

Component-based Program Synthesis in OCaml
Zhanpeng Liang, Kanae Tsushima
(extended abstract)

Extending OCaml's open
Runhang Li, Jeremy Yallop
(extended abstract, iOCamlJS playground!, additional material)

Genspio: Generating Shell Phrases In OCaml
Sebastien Mondet
(extended abstract, slides, code)

Owl: A General-Purpose Numerical Library in OCaml
Liang Wang
(extended abstract from arXiv, presentation)

ROTOR: First Steps Towards a Refactoring Tool for OCaml
Reuben N. S. Rowe, Simon Thompson
(extended abstract, slides, code, Docker image)

Testing with Crowbar
Stephen Dolan, Mindy Preston

Bioinformatics, The Typed Tagless Final Way
Sebastien Mondet
(extended abstract, slides, code)

Tezos: the OCaml Crypto-Ledger
Benjamin Canou, Grégoire Henry, Pierre Chambart, Fabrice Le Fessant, Arthur Breitman

The State of the OCaml Platform: September 2017
Anil Madhavapeddy
(slides)

Wodan: a pure OCaml, flash-aware filesystem library
Gabriel de Perthuis
(extended abstract)

ocamli: Interpreted OCaml
John Whitington
(extended abstract)

mSAT: An OCaml SAT Solver
Bury Guillaume
(extended abstract)

Tyre – Typed Regular Expressions
Gabriel Radanne
(abstract)

Jbuilder: a modern approach to OCaml development
Jeremie Dimino, Mark Shinwell