Linear Exponentials as Graded Modal Types - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2021

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.
Fichier principal
Vignette du fichier
TLLA_2021_paper_11.pdf (243.46 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

lirmm-03271465 , version 1 (25-06-2021)

Licence

Identifiers

  • HAL Id : lirmm-03271465 , version 1

Cite

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⟩
602 View
503 Download

Share

More