ICFP 2016- Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Full Citation in the ACM Digital Library

SESSION: Invited Talks

TensorFlow: learning functions at scale

Journey to find bugs in JavaScript web applications in the wild

A functional programmer's guide to homotopy type theory

SESSION: Session 1

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

Dag-calculus: a calculus for parallel computation

A lambda-calculus foundation for universal probabilistic programming

Deriving a probability density calculator (functional pearl)

SESSION: Session 2

A new verified compiler backend for CakeML

Sequent calculus as a compiler intermediate language

Refinement through restraint: bringing down the cost of verification

SESSION: Session 3

Fully abstract compilation via universal embedding

Oh Lord, please don't let contracts be misunderstood (functional pearl)

A type theory for incremental computational complexity with control flow changes

SESSION: Session 4

Compact bit encoding schemes for simply-typed lambda-terms

Queueing and glueing for optimal partitioning (functional pearl)

All sorts of permutations (functional pearl)

SESSION: Session 5

A glimpse of Hopjs

Experience report: growing and shrinking polygons for random testing of computational geometry algorithms

Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing

Datafun: a functional Datalog

SESSION: Session 6

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong)

Automatically disproving fair termination of higher-order functional programs

Higher-order ghost state

SESSION: Session 7

Unifiers as equivalences: proof-relevant unification of dependently typed data

Elaborator reflection: extending Idris in Idris

Partial type equivalences for verified dependent interoperability

SESSION: Session 8

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory

An abstract memory functor for verified C static analyzers

SESSION: Session 9

Ghostbuster: a tool for simplifying and converting GADTs

Indexed codata types

Disjoint intersection types

Set-theoretic types for polymorphic variants

SESSION: Session 10

Hierarchical memory management for parallel programs

Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis

A fully concurrent garbage collector for functional programs on multicore processors

SESSION: Session 11

Talking bananas: structural recursion for session types

The best of both worlds: linear functional programming without compromise

Context-free session types

SESSION: Session 12

Combining effects and coeffects via grading

String diagrams for free monads (functional pearl)