2026-07-22T20:50:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13458 2024-03-06T10:52:08Z ddc:004 open_access

A Deep Quantitative Type System Guerrieri, Giulio Heijltjes, Willem B. Paulus, Joseph W.N. Lambda-calculus Deep inference Intersection types Resource calculus 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Giulio Guerrieri and Willem B. Heijltjes and Joseph W.N. Paulus 2021 Is Part Of LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2021.24 urn:nbn:de:0030-drops-134586 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.24 eng https://creativecommons.org/licenses/by/3.0/legalcode