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

https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271465
Contributor : Isabelle Gouat <>
Submitted on : Friday, June 25, 2021 - 5:46:34 PM
Last modification on : Friday, June 25, 2021 - 7:11:57 PM

File

TLLA_2021_paper_11.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NonCommercial 4.0 International License

Identifiers

  • HAL Id : lirmm-03271465, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

64

Files downloads

42