π with leftovers: a mechanisation in Agda

Uma Zalakain, Ornela Dardha

Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across su…