A deep quantitative type system

Research output: Contribution to conferencePaper

24 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
Publication statusPublished - 2021

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

Cite this