WG211/M12Igarashi

Revisiting Cross-Stage Persistence by Itsushi Igarashi (joint work with Yuichiro Hanada)

One of the distinguishing features of MetaOCaml is cross-stage persistence (CSP) with which a variable defined at an earlier stage can be referred to at a later stage. It allows, for example, library functions to be used inside quotation. However, the semantics of CSP formalized in \lambda^\alpha is known to be complex. We discuss another semantics of CSP formalized from a different perspective and try to deepen the understanding why it is (or has to be) complex.