A deep quantitative type system

Giulio Guerrieri, Willem Heijltjes, Joseph Paulus

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

1 Citation (SciVal)
55 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
Subtitle of host publicationCSL 2021
EditorsChristel Baier, Jean Goubault-Larrecq
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages24
ISBN (Electronic)9783959771757
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 Informatics, LIPIcs
ISSN (Print)1868-8969


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


  • Deep inference
  • Intersection types
  • Lambda-calculus
  • Resource calculus

ASJC Scopus subject areas

  • Software

Cite this