Semantic Bounds and Multi Types, Revisited - Laboratoire d'informatique de l'X (LIX)
Communication Dans Un Congrès Année : 2024

Semantic Bounds and Multi Types, Revisited

Résumé

Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms. In the last few years, de Carvalho’s work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type derivations, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to type substitutions. It is however also the most interesting, because it shows that the bounding power is inherent to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system. Here we dissect and clarify the second part of de Carvalho’s work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.
Fichier principal
Vignette du fichier
LIPIcs.CSL.2024.7.pdf (998.7 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
licence

Dates et versions

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

Licence

Identifiants

Citer

Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. ⟨10.4230/LIPIcs.CSL.2024.7⟩. ⟨hal-04837714⟩
0 Consultations
0 Téléchargements

Altmetric

Partager

More