arXiv subjects

Hector Gramaglia

Publications and source records attributed to Hector Gramaglia.

3 recordsLinked to original sources

arXiv2025

Weak-Linear Types

Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle, and guarantee safe deallocation. The use of linear types encounters limitations in practice, since linear data, in the traditional sense, do not so often appear in actual programs. Several alternatives have been proposed in the attempt to relax the condition of linearity, adding coercions to the language to allow linear objects to be temporarily aliased. In this work we propose a new alternative, whose virtue is to preserve the simplicity and elegance of the original system.

cs.PL↗

arXiv2025

Globality and Regions

We obtain a characterization of global variables by unifying abstraction with region abstraction in a region-based language. More precisely, in a previous work a language called global was presented, whose virtue is to provide a conceptually clear way of introducing imperative operations in a functional language. Memory safety is provided by the concept of linear protection, which connects the global system to a linear one. In this paper we show that the concept of global variable provided by the global language arises from the Tofte and Talping's region language through the unification of abstraction and region abstraction.

cs.PL↗

arXiv2024

Weak-linearity, globality and in-place update

Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle. This has promoted numerous investigations into safe introduction of in-place update. Various type systems have been proposed for this aim, but the memory management that promotes linear evaluation does not adequately model the destruction of in-place update. The main achievement of this work is to establish a simple theoretical framework that will allow us to clarify the potential (and limits) of linearity to guarantee the process of transforming a functional program into an imperative one. For this purpose we will introduce a type system called "global" that will model the in-place update as the linear system models the one-time use.

cs.PL↗