Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic

This paper introduces the exponential substitution calculus (ESC), a new presentation of cut elimination for IMELL, based on proof terms and building on the idea that exponentials can be seen as explicit substitutions. The idea in itself is not new, but here it is pushed to a new level, inspired by...

Full description

Bibliographic Details
Main Author: Beniamino Accattoli
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2023-12-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/10888/pdf