An Agda mechanisation of a graded coeffect calculus.
This has been used to prove a generalised non-interference theorem in the paper "On Graded Coeffect Types for Information-Flow Control" (Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard, Vineet Rajani, Michael Vollmer, 2025).