Linearization via Rewriting (Long Version)
Logic in Computer Science
2025-03-26 v2 Programming Languages
Abstract
We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its linearization. The calculus is shown to be normalizing and confluent. Noticeably, every strongly normalizable lambda-term can be represented by a type derivation. This is the first example of a system where the linearization process takes place internally, while remaining purely finitary and rewrite-based.
Keywords
Cite
@article{arxiv.2503.04408,
title = {Linearization via Rewriting (Long Version)},
author = {Ugo Dal Lago and Federico Olimpieri},
journal= {arXiv preprint arXiv:2503.04408},
year = {2025}
}