Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Mon 19 Sep 2016 16:05 - 16:30 at Noh Theater - Session 3 Chair(s): Neel Krishnaswami

Incremental computation aims to speed up re-runs of a program after
its inputs have been modified slightly. It works by recording a trace
of the program's first run and propagating changes through the trace
in incremental runs, trying to re-use as much of the original trace as
possible. The recent work CostIt is a type and effect system to
establish the time complexity of incremental runs of a program, as a
function of input changes. However, CostIt is limited in two
ways. First, it prohibits input changes that influence control
flow. This makes it impossible to type programs that, for instance,
branch on inputs that may change. Second, the soundness of CostIt
is proved relative to an abstract cost semantics, but it is unclear
how the semantics can be realized.

In this paper, we address both these limitations. We present DuCostIt,
a re-design of CostIt, that combines reasoning about costs of
change propagation and costs of from-scratch evaluation. The latter
lifts the restriction on control flow changes. To obtain the type
system, we refine Flow Caml, a type system for information flow
analysis, with cost effects. Additionally, we inherit from CostIt
index refinements to track data structure sizes and a co-monadic
type. Using a combination of binary and unary step-indexed logical
relations, we prove DuCostIt's cost analysis sound relative to not
only an abstract cost semantics, but also a concrete semantics, which
is obtained by translation to an ML-like language.

Mon 19 Sep
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

15:15 - 16:30
Session 3Research Papers at Noh Theater
Chair(s): Neel KrishnaswamiUniversity of Birmingham, UK
Fully Abstract Compilation via Universal Embedding
Research Papers
Max NewNortheastern University, William J. BowmanNortheastern University, Amal AhmedNortheastern University
Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Research Papers
Christos DimoulasHarvard University, Max NewNortheastern University, Robby FindlerNorthwestern University, Matthias FelleisenNortheastern University
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Research Papers
Ezgi ÇiçekMPI-SWS, Germany, Zoe ParaskevopoulouPrinceton University, USA, Deepak GargMPI-SWS, Germany