Jacques Garrigue, Gabriele Keller, Eijiro Sumii
Proceedings of the 21st International Conference on Functional Programming
ICFP, 2016.

@proceedings{ICFP-2016,
	doi           = "10.1145/2951913",
	editor        = "Jacques Garrigue and Gabriele Keller and Eijiro Sumii",
	isbn          = "978-1-4503-4219-3",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 21st International Conference on Functional Programming}",
	year          = 2016,
}

Contents (40 items)

ICFP-2016-Abadi #learning #named #scalability

TensorFlow: learning functions at scale (MA), p. 1.

ICFP-2016-Ryu #debugging #javascript #web

Journey to find bugs in JavaScript web applications in the wild (SR), p. 2.

ICFP-2016-Licata #functional #type system

A functional programmer's guide to homotopy type theory (DL), p. 3.

ICFP-2016-CastroHS #morphism #parallel #pipes and filters #process #reasoning #using

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms (DC, KH, SS), pp. 4–17.

ICFP-2016-AcarCRS #calculus #named #parallel

Dag-calculus: a calculus for parallel computation (UAA, AC, MR, FS), pp. 18–32.

ICFP-2016-BorgstromLGS #probability #programming #λ-calculus

A lambda-calculus foundation for universal probabilistic programming (JB, UDL, ADG, MS), pp. 33–46.

ICFP-2016-IsmailS #functional #probability

Deriving a probability density calculator (functional pearl) (WMI, CcS), pp. 47–59.

ICFP-2016-TanMKFON #compilation

A new verified compiler backend for CakeML (YKT, MOM, RK, ACJF, SO, MN), pp. 60–73.

ICFP-2016-DownenMAJ #calculus #compilation

Sequent calculus as a compiler intermediate language (PD, LM, ZMA, SPJ), pp. 74–88.

ICFP-2016-OConnorCRALMNSK #cost analysis #refinement #verification

Refinement through restraint: bringing down the cost of verification (LO, ZC, CR, SA, JL, TCM, YN, TS, GK), pp. 89–102.

ICFP-2016-NewBA #compilation

Fully abstract compilation via universal embedding (MSN, WJB, AA), pp. 103–116.

ICFP-2016-DimoulasNFF #contract #functional

Oh Lord, please don't let contracts be misunderstood (functional pearl) (CD, MSN, RBF, MF), pp. 117–131.

ICFP-2016-CicekP0 #complexity #control flow #incremental #type system

A type theory for incremental computational complexity with control flow changes (EÇ, ZP, DG0), pp. 132–145.

ICFP-2016-Takeda0YS #encoding #λ-calculus

Compact bit encoding schemes for simply-typed lambda-terms (KT, NK0, KY, AS), pp. 146–157.

ICFP-2016-MuCL #clustering #functional

Queueing and glueing for optimal partitioning (functional pearl) (SCM, YHC, YHL), pp. 158–167.

ICFP-2016-ChristiansenDD #functional #permutation

All sorts of permutations (functional pearl) (JC, ND, SD), pp. 168–179.

ICFP-2016-SerranoP

A glimpse of Hopjs (MS, VP), pp. 180–192.

ICFP-2016-Sergey #algorithm #case study #experience #geometry #random testing #testing

Experience report: growing and shrinking polygons for random testing of computational geometry algorithms (IS), pp. 193–199.

ICFP-2016-EmotoMHMI #domain-specific language #exclamation #functional #graph

Think like a vertex, behave like a function! a functional DSL for vertex-centric big graph processing (KE, KM, ZH, AM, HI), pp. 200–213.

ICFP-2016-ArntzeniusK #datalog #functional #named

Datafun: a functional Datalog (MA, NRK), pp. 214–227.

ICFP-2016-SeidelJW #fault #source code #static typing

Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong) (ELS, RJ, WW), pp. 228–242.

ICFP-2016-WatanabeST0 #automation #functional #higher-order #source code #termination

Automatically disproving fair termination of higher-order functional programs (KW, RS, TT, NK0), pp. 243–255.

ICFP-2016-JungKBD #higher-order

Higher-order ghost state (RJ, RK, LB, DD), pp. 256–269.

ICFP-2016-CockxDP #unification

Unifiers as equivalences: proof-relevant unification of dependently typed data (JC, DD, FP), pp. 270–283.

ICFP-2016-ChristiansenB

Elaborator reflection: extending Idris in Idris (DRC, EB), pp. 284–297.

ICFP-2016-DagandTT

Partial type equivalences for verified dependent interoperability (PÉD, NT, ÉT), pp. 298–310.

ICFP-2016-DaraisH #framework

Constructive Galois connections: taming the Galois connection framework for mechanized metatheory (DD, DVH), pp. 311–324.

ICFP-2016-BlazyLP #c #memory management

An abstract memory functor for verified C static analyzers (SB, VL, DP), pp. 325–337.

ICFP-2016-McDonellZCN #data type #named

Ghostbuster: a tool for simplifying and converting GADTs (TLM, TAKZ, MC, RRN), pp. 338–350.

ICFP-2016-ThibodeauCP #data type

Indexed codata types (DT, AC, BP), pp. 351–363.

ICFP-2016-OliveiraSA

Disjoint intersection types (BCdSO, ZS, JA), pp. 364–377.

ICFP-2016-CastagnaP0 #polymorphism

Set-theoretic types for polymorphic variants (GC, TP, KN0), pp. 378–391.

ICFP-2016-RaghunathanMAB #memory management #parallel #source code

Hierarchical memory management for parallel programs (RR, SKM, UAA, GEB), pp. 392–406.

ICFP-2016-Gilray0M #analysis #control flow

Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis (TG, MDA0, MM), pp. 407–420.

ICFP-2016-UenoO #concurrent #functional #garbage collection #manycore #source code

A fully concurrent garbage collector for functional programs on multicore processors (KU, AO), pp. 421–433.

ICFP-2016-LindleyM #recursion

Talking bananas: structural recursion for session types (SL, JGM), pp. 434–447.

ICFP-2016-Morris #functional #linear #programming

The best of both worlds: linear functional programming without compromise (JGM), pp. 448–461.

ICFP-2016-ThiemannV

Context-free session types (PT0, VTV), pp. 462–475.

ICFP-2016-GaboardiKOBU

Combining effects and coeffects via grading (MG, SyK, DAO, FB, TU), pp. 476–489.

ICFP-2016-PirogW #diagrams #for free #functional #monad #string

String diagrams for free monads (functional pearl) (MP, NW), pp. 490–501.