List types for resource aware languages: an implicit name approach

TL;DR

This paper introduces a formal framework for variable control in resource-aware languages using implicit names and list types, including implementations and novel concepts for managing linearity.

Contribution

It presents a new formalisation of variable control with implicit names, introduces list types for linearity, and provides a Haskell implementation.

Findings

Formalisation of variable control with implicit names

Introduction of list types for linearity management

Implementation in Haskell demonstrating practicality

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.