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

Displayed time zone: Osaka, Sapporo, Tokyo change

15:15 - 16:30
Session 3Research Papers at Noh Theater
Chair(s): Neel Krishnaswami University of Birmingham, UK
Fully Abstract Compilation via Universal Embedding
Research Papers
Max S. New Northeastern University, William J. Bowman Northeastern University, Amal Ahmed Northeastern University
Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Research Papers
Christos Dimoulas Harvard University, Max S. New Northeastern University, Robert Bruce Findler Northwestern University, Matthias Felleisen Northeastern University
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Research Papers
Ezgi Çiçek MPI-SWS, Germany, Zoe Paraskevopoulou Princeton University, USA, Deepak Garg MPI-SWS, Germany