Related?

[Bersier]

Disclaimer: unfortunately, I have little familiarity with this experiment.

Looking at the beginning of the paper Tracking Captured Variables in Types, I got reminded of Professor Pientka's work on Beluga. One of her earliest papers on that topic seems to be Contextual Modal Type Theory.

Is there more than a superficial resemblance between her work and this experiment? I'm posting this just in case it's useful to anyone.

[abgruszecki]

Yes, CMTT is related to Capture Tracking. The "boxing" construct in CC has been basically co-developed with boxing in System C (formal foundations for the Effekt lang), as described in this recent paper : https://dl.acm.org/doi/abs/10.1145/3527320 . You can find a comparison with CMTT in the related work section.