A deep quantitative type system

Research output: Chapter in Book/Report/Conference proceedingConference contribution

48 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
Subtitle of host publicationCSL 2021
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages24:1-24:24
Number of pages24
Volume183
Edition2021
ISBN (Print)978-3-95977-175-7
DOIs
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

Conference

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

Cite this