2021/05/25 by Boruch-Gruszecki, Aleksander, Brachthäuser, Jonathan Immanuel, Lee, Edward +2
#68N15 #D.3.1 #FOS: Computer and information sciences #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2105.11896
Type systems usually characterize the shape of values but not their free variables. However, there are many desirable safety properties one could guarantee if one could track how references can escape. For example, one may implement algebraic effect handlers using capabilities -- a value which permits one to perform the effect -- safely if one can guarantee that the capability itself does not escape the scope bound by the effect handler. To this end, we study the \textrmCF_