Kind of - but more about dynamic dispatch / overloaded function name resolution than protection per se. Furthermore, the decorations work at the lowest possibl

Kind of - but more about dynamic dispatch / overloaded function name resolution than protection per se. Furthermore, the decorations work at the lowest possible level, and are bound up with the extended beta reduction (there is also an unwrap operator with associated reduction rules). Of course, any computation can be modelled in the standard lambda calculus, without needing to hack the reduction, but I believe that this extension is in some sense non-trivial as it would require the LC to first implement the LC terms and usual beta reduction within itself, before then implementing the additional terms and redux.