Formalizing dynamic-wind in the lambda calculus
Ryotaro Kasuga, Shin-ya Nishizaki · 2022
The Scheme programming language has the control constructs: call-with-current-continuation (call/cc) and dynamic-wind. The construct call/cc is a procedure to handle first-class continuations. The construct dynamic-wind is a procedure to hook a continuation captured by call/cc. It can add pre- and post-processing to a continuation, and allows flexible handling of global escape and control effect by continuation calls. The first example where the continuation is applied is rewriting variables with dynamic scope, and the second is saving and restoring registers during context switching of threads implemented in user space.