From Algebra to Abstract Machine: A Verified Generic Construction
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 Sep Times are displayed in time zone: (GMT-05:00) Guadalajara, Mexico City, Monterrey change
|14:20 - 14:45|
Daan LeijenMicrosoft Research, USADOI
|14:45 - 15:10|
Carlos Tomé CortiñasUtrecht University, Netherlands, Wouter SwierstraUtrecht University, NetherlandsDOI