Type-based Allocation Analysis for Co-Recursion in Lazy Functional Languages
This paper presents a novel type-and-effect analysis for predicting upper-bounds on memory allocation costs for co-recursive definitions in a simple lazily-evaluated functional language. We show the soundness of this system against an instrumented variant of Launchbury’s semantics for lazy evaluation which serves as a formal cost model. Our soundness proof requires an intermediate semantics employing indirections. Our proof of correspondence between these semantics that we provide is thus a crucial part of this work.
Thu 16 Apr
|16:30 - 17:00|
Wilmer RicciottiUniversity of Toulouse
|17:00 - 17:30|
|17:30 - 18:00|