A Deep Quantitative Type System

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

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

3 Downloads (Pure)

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 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
Pages24:1-24:24
Number of pages24
ISBN (Print)978-3-95977-175-7
DOIs
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
Volume183
ISSN (Electronic)1868-8969

Conference

Conference29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
CountrySlovenia
CityLubijana
Period25/01/202128/01/2021

Cite this