Projects per year
Abstract
We investigate intersection types and resource lambdacalculus in deepinference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersectiontyped lambdacalculus, and simplytyped lambdacalculus; it accommodates both idempotence and nonidempotence; 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 language  English 

Publication status  Published  2021 
Fingerprint Dive into the research topics of 'A deep quantitative type system'. Together they form a unique fingerprint.
Projects
 1 Active

Typed LambdaCalculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 31/12/21
Project: Research council