Abstract
We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the “collection calculus”, as a Curry–Howard interpretation of the type system, that embodies these computational properties.
Original language | English |
---|---|
Title of host publication | 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) |
Editors | Christel Baier, Jean Goubault-Larrecq |
Place of Publication | Dagstuhl, Germany |
Publisher | Schloss Dagstuhl--Leibniz-Zentrum für Informatik |
Pages | 24:1-24:24 |
Number of pages | 24 |
ISBN (Print) | 978-3-95977-175-7 |
DOIs | |
Publication status | Published - 2021 |
Event | 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia Duration: 25-Jan-2021 → 28-Jan-2021 |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Publisher | Schloss Dagstuhl |
Volume | 183 |
ISSN (Electronic) | 1868-8969 |
Conference
Conference | 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) |
---|---|
Country/Territory | Slovenia |
City | Lubijana |
Period | 25/01/2021 → 28/01/2021 |