Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Isabelle Gouat <>
Submitted on : Friday, June 25, 2021 - 5:46:34 PM
Last modification on : Friday, June 25, 2021 - 7:11:57 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License


  • HAL Id : lirmm-03271465, version 1



Jack Hughes, Daniel Marshall, James Wood, Dominic Orchard. Linear Exponentials as Graded Modal Types. 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), Jun 2021, Rome (virtual), Italy. ⟨lirmm-03271465⟩



Record views


Files downloads