Factoring derivation spaces via intersection types

DOI10.1007/978-3-030-02768-1_2zbMATH Open1519.68043arXiv1907.08820OpenAlexW2897574255MaRDI QIDQ6166134FDOQ6166134

Authors: Pablo Barenbaum, Gonzalo Ciruelos 

Publication date: 2 August 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the lambda-calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the lambda-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a lambda-term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.

Full work available at URL: https://arxiv.org/abs/1907.08820

Recommendations

• Intersection types for the resource control lambda calculi
• scientific article; zbMATH DE number 7204443
• Intersection types for explicit substitutions
• Non-idempotent intersection types and strong normalisation
• Intersection types for λGtz-calculus

zbMATH Keywords

lambda-calculusintersection typesderivation space

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

This page was built for publication: Factoring derivation spaces via intersection types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166134)