A deep quantitative type system

Giulio Guerrieri, Willem Heijltjes, Joseph Paulus

Research output: Chapter in Book/Report/Conference proceedingChapter in a published conference proceeding

1 Citation (SciVal)
50 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
Subtitle of host publicationCSL 2021
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages24
ISBN (Print)978-3-95977-175-7
Publication statusPublished - 13 Jan 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 Informations (LIPIcs)
PublisherSchloss Dagstuhl
ISSN (Electronic)1868-8969


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


Dive into the research topics of 'A deep quantitative type system'. Together they form a unique fingerprint.

Cite this