Proceedings of the 24th International Conference on Functional Programming
ICFP-2019, 2019.

@proceedings{ICFP-2019,
	journal       = "{Proceedings of the ACM on Programming Languages}",
	month         = "August",
	number        = "ICFP",
	title         = "{Proceedings of the 24th International Conference on Functional Programming}",
	volume        = 3,
	year          = 2019,
}

Contents (39 items)

ICFP-2019-FlattDDKMSTZ #case study #experience

Rebuilding racket on chez scheme (experience report) (MF, CD, RKD, AWK, GEM, SS, STH, JZ), p. 15.

ICFP-2019-HameerP #automation #case study #education #experience #functional #programming #using

Teaching the art of functional programming using automated grading (experience report) (AH, BP), p. 15.

ICFP-2019-ChristiansenDDH #case study #experience #haskell #industrial

Dependently typed Haskell in industry (experience report) (DTC, ISD, RD, JH, TR), p. 16.

ICFP-2019-YallopW #case study #experience #named

Lambda: the ultimate sublanguage (experience report) (JY, LW), p. 17.

ICFP-2019-AlgehedB #parametricity

Simple noninterference from parametricity (MA, JPB), p. 22.

ICFP-2019-HackettH #call-by

Call-by-need is clairvoyant call-by-value (JH, GH), p. 23.

ICFP-2019-Morihata #algebra #equation #parallel #reasoning #reduction #λ-calculus

Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning (AM), p. 25.

ICFP-2019-KissFEJ #haskell #higher-order #programming

Higher-order type-level programming in Haskell (CK, TF, SE, SPJ), p. 26.

ICFP-2019-SwierstraB #functional #semantics

A predicate transformer semantics for effects (functional pearl) (WS, TB), p. 26.

ICFP-2019-BahrGM #calculus #programming

Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks (PB, CG, REM), p. 27.

ICFP-2019-BottuXMS

Coherence of type class resolution (GJB, NX, KM, TS), p. 28.

ICFP-2019-CongOER #compilation #continuation

Compiling with continuations, or without? whatever (YC, LO, GME, TR), p. 28.

ICFP-2019-LewchenkoRGC #programming

Sequential programming for replicated data stores (NVL, AR, AG, PC), p. 28.

ICFP-2019-MiltnerMFPWZ #lens #symmetry

Synthesizing symmetric lenses (AM, SM, KF, BCP, DW, SZ), p. 28.

ICFP-2019-TimanyB #concurrent #continuation #relational #source code #verification

Mechanized relational verification of concurrent programs with continuations (AT, LB), p. 28.

ICFP-2019-ZhangRHP0 #difference #logic #named #privacy

Fuzzi: a three-level logic for differential privacy (HZ, ER, AH, BCP, AR0), p. 28.

ICFP-2019-DelawareSPYC #named

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats (BD, SS, CPC, QY, AC), p. 29.

ICFP-2019-GratzerSB #dependent type #implementation #type system

Implementing a modal dependent type theory (DG, JS, LB), p. 29.

ICFP-2019-LindenhoviusMZ #linear #recursion

Mixed linear and non-linear recursive types (BL, MWM, VZ), p. 29.

ICFP-2019-MaillardAAMHRT #monad

Dijkstra monads for all (KM, DA, RA, GM, CH, ER, ÉT), p. 29.

ICFP-2019-MiraldoS #algorithm #difference #performance #type safety

An efficient algorithm for type-safe structural diffing (VCM, WS), p. 29.

ICFP-2019-MokhovLMD

Selective applicative functors (AM, GL, SM, JD), p. 29.

ICFP-2019-Paraskevopoulou

Closure conversion is safe for space (ZP, AWA), p. 29.

ICFP-2019-PattersonA #compilation #correctness #functional #theorem

The next 700 compiler correctness theorems (functional pearl) (DP, AA), p. 29.

ICFP-2019-PedrotTFT #type system

A reasonably exceptional type theory (PMP, NT, HJF, ÉT), p. 29.

ICFP-2019-QuG0 #cost analysis #relational #source code

Relational cost analysis for functional-imperative programs (WQ, MG, DG0), p. 29.

ICFP-2019-ShermanMC #modelling #robust

Sound and robust solid modeling via exact real arithmetic and continuity (BS, JM, MC), p. 29.

ICFP-2019-SmithA #source code

Synthesizing differentially private programs (CS, AA), p. 29.

ICFP-2019-SozeauM #coq #equation #functional #programming #proving

Equations reloaded: high-level dependently-typed functional programming and proving in Coq (MS, CM), p. 29.

ICFP-2019-StrydonckPD #compilation #linear

Linear capabilities for fully abstract compilation of separation-logic-verified code (TVS, FP, DD), p. 29.

ICFP-2019-VezzosiM0 #induction #programming language

Cubical agda: a dependently typed programming language with univalence and higher inductive types (AV, AM, AA0), p. 29.

ICFP-2019-WeirichCVE #dependent type #haskell

A role for dependent types in Haskell (SW, PC, AV, RAE), p. 29.

ICFP-2019-ZhaoOS #formal method #polymorphism #type inference

A mechanical formalization of higher-ranked polymorphic type inference (JZ, BCdSO, TS), p. 29.

ICFP-2019-EremondiTG #approximate #dependent type #normalisation

Approximate normalization for gradual dependent types (JE, ÉT, RG), p. 30.

ICFP-2019-MullerWA #parallel

Fairness in responsive parallelism (SKM, SW, UAA), p. 30.

ICFP-2019-OrchardLE #reasoning

Quantitative program reasoning with graded modal types (DO, VBL, HEI), p. 30.

ICFP-2019-ShaikhhaFVJ #functional #performance #programming

Efficient differentiable programming in a functional array-processing language (AS, AF, DV, SPJ), p. 30.

ICFP-2019-WaliaNCTS #algorithm #performance

From high-level inference algorithms to efficient code (RW, PN, JC, STH, CcS), p. 30.

ICFP-2019-WangZDWER #programming

Demystifying differentiable programming: shift/reset the penultimate backpropagator (FW, DZ, JMD, XW, GME, TR), p. 31.