ICFP 2018 (series) / TyDe 2018 (series) / Type-Driven Development /
From Algebra to Abstract Machine: A Verified Generic Construction
Thu 27 Sep 2018 14:45 - 15:10 at New York Central - Effect Handlers & Abstract Machine Chair(s): Niki Vazou
Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tail-recursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tail-recursive higher-order function that is guaranteed to produce the same result as the fold. Doing so combines the compositional nature of folds and the performance benefits of a hand-written tail-recursive function in a single setting.
Thu 27 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
Thu 27 Sep
Displayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 15:10 | Effect Handlers & Abstract MachineTyDe at New York Central Chair(s): Niki Vazou University of Maryland, USA | ||
14:20 25mResearch paper | First Class Dynamic Effect Handlers: or, Polymorphic Heaps with Dynamic Effect Handlers TyDe Daan Leijen Microsoft Research, USA DOI | ||
14:45 25mResearch paper | From Algebra to Abstract Machine: A Verified Generic Construction TyDe Carlos Tomé Cortiñas Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands DOI |