Linear Exponentials as Graded Modal Types
Abstract
Graded type systems, which allow resource usage in programs to be tracked and reasoned about, are proliferating in recent works. These systems generalise ideas from Bounded Linear Logic (BLL), which allows the exponential modality ! from linear logic to be indexed by a bound on the number of times a formula is used. Graded systems generalise BLL's indexed modality to an arbitrary semiring of grades. Despite their relation to linear logic, particular choices in most graded type systems mean they cannot faithfully model ! due to the interaction between ! and ⊗; there are certain distributive laws that can be derived in graded type systems but cannot be derived in linear logic. We remedy this by enriching the structure of the grading with an additional operation, and show how this recovers the expressive power of Intuitionistic Multiplicative Exponential Linear Logic (IMELL) in a system with graded modal types. We briefly discuss our implementation involving this new operation for the graded modal language Granule.
Origin | Files produced by the author(s) |
---|