IMELL Cut Elimination with Linear Overhead - Laboratoire d'informatique de l'X (LIX)
Communication Dans Un Congrès Année : 2024

IMELL Cut Elimination with Linear Overhead

Résumé

Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Fichier principal
Vignette du fichier
LIPIcs.FSCD.2024.24.pdf (956.37 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
licence

Dates et versions

hal-04837719 , version 1 (13-12-2024)

Licence

Identifiants

Citer

Beniamino Accattoli, Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Jul 2024, Tallin, Estonia. ⟨10.4230/LIPICS.FSCD.2024.24⟩. ⟨hal-04837719⟩
0 Consultations
0 Téléchargements

Altmetric

Partager

More