Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

List types for resource aware languages: an implicit name approach

Silvia Ghilezan, Jelena Ivetić, Pierre Lescanne, Simona Kašterović

TL;DR

Three calculi with implicit naming are introduced: $'L^{\mathcal{L}}$, $\Lambda^{\mathcal{L}}_\upsilon$, and $'L_{\textrm{\textregistered}}^{\mathcal{L}}$, each equipped with a unifying $\mathcal{L}$-type system to directly characterize linearity in the presence of implicit names. The authors prove $\mathcal{L}$-type preservation under reduction for the explicit-substitution and resource-controlled calculi and provide a practical Haskell implementation with read/readback translations that connect to the standard $\Lambda$-calculus. Through a bestiary of terms and concrete reductions (including SKK, booleans, and Church numerals), the work demonstrates how resource control (duplication/erasure) interacts with implicit naming. The framework offers a direct, implementable approach to resource-aware compilation and formalizes linearity in implicit-name settings, laying groundwork for integration with traditional type systems and broader linguistic applications.

Abstract

A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names, implicit substitution and resource control. We propose a novel concept of list types, which are used to give a simple and manageable definition of linearity. We develop an implementation in Haskell.

List types for resource aware languages: an implicit name approach

TL;DR

Three calculi with implicit naming are introduced: , , and , each equipped with a unifying -type system to directly characterize linearity in the presence of implicit names. The authors prove -type preservation under reduction for the explicit-substitution and resource-controlled calculi and provide a practical Haskell implementation with read/readback translations that connect to the standard -calculus. Through a bestiary of terms and concrete reductions (including SKK, booleans, and Church numerals), the work demonstrates how resource control (duplication/erasure) interacts with implicit naming. The framework offers a direct, implementable approach to resource-aware compilation and formalizes linearity in implicit-name settings, laying groundwork for integration with traditional type systems and broader linguistic applications.

Abstract

A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names, implicit substitution and resource control. We propose a novel concept of list types, which are used to give a simple and manageable definition of linearity. We develop an implementation in Haskell.
Paper Structure (18 sections, 14 theorems, 95 equations, 13 figures)

This paper contains 18 sections, 14 theorems, 95 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Terms with implicit names $\Lambda$
  3. Restricted terms $'L^{\mathcal{L}}$
  4. $\mathcal{L}$-types for $'L^{\mathcal{L}}$
  5. Remark
  6. Restricted terms with explicit substitution $\Lambda^{\mathcal{L}}_\upsilon$
  7. $\mathcal{L}$-types for $\Lambda^{\mathcal{L}}_\upsilon$
  8. Reduction of $\Lambda^{\mathcal{L}}_\upsilon$
  9. Extended terms with resource control $'L_{\textrm{\textregistered}}$
  10. A bestiary of $'l_{\textrm{\textregistered}}$-terms
  11. $\mathcal{L}$-types for $'L_{\textrm{\textregistered}}^{\mathcal{L}}$
  12. Resource reduction in $'L_{\textrm{\textregistered}}$
  13. Head-reduction and $\beta$-contraction in $'L_{\textrm{\textregistered}}^{\mathcal{L}}$
  14. $\mathcal{L}$-type preservation for substitution
  15. Examples of reductions in $'l_{\textrm{\textregistered}}$-calculus : SKK and booleans
  16. ...and 3 more sections

Key Result

Proposition 1

If $t : \ell$ then $\ell$ is sorted.

Figures (13)

  • Figure 1: Bourbaki assembly in https://books.google.fr/books?id=VDGifaOQogcC&pg=SA1-PA14&dq=Bourbaki+ensemble+signes+assemblages
  • Figure 2: Bourbaki assembly of $\mathsf{SK}$
  • Figure 3: The term SK and its three contractions
  • Figure 4: Terms with duplicators and erasures
  • Figure 5: The rewriting system for $\lambda\upsilon$-calculus
  • ...and 8 more figures

Theorems & Definitions (54)

  • Definition 1: $\mathcal{L}$-types
  • Definition 2: Merge
  • Remark 1
  • Definition 3: Decrement
  • Definition 4: Terms $'L^{\mathcal{L}}$
  • Proposition 1: Sortedness of lists
  • proof
  • Example 1: Typing terms
  • Proposition 2: Combinators in $'L^{\mathcal{L}}$
  • proof
  • ...and 44 more