Linear Exponentials as Graded Modal Types - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Linear Exponentials as Graded Modal Types

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Licence

Paternité - Pas d'utilisation commerciale

Identifiants

  • HAL Id : lirmm-03271465 , version 1

Citer

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⟩
522 Consultations
453 Téléchargements

Partager

Gmail Facebook X LinkedIn More