A Deep Quantitative Type System

Giulio Guerrieri, Willem B. Heijltjes, Joseph W. N. Paulus

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
32 Downloads (Pure)


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 languageEnglish
Title of host publication29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
EditorsChristel Baier, Jean Goubault-Larrecq
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Number of pages24
ISBN (Print)978-3-95977-175-7
Publication statusPublished - 2021
Event29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
- Lubijana, Slovenia
Duration: 25-Jan-202128-Jan-2021

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl
ISSN (Electronic)1868-8969


Conference29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Cite this