piyush-kurur / icfp2016-papers Goto Github PK

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.

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

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

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)

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.

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

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.

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.

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.

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
S. Peyton Jones, R. Eisenberg, G. Érdi, M. Pickering.

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

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

Supermonads
J. Bracker, H. Nilsson.

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

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

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