1 Search Results for "Paulus, Joseph W.N."

Document

DOI: 10.4230/LIPIcs.CSL.2021.24

A Deep Quantitative Type System

Authors: Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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.

Cite as

Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus. A Deep Quantitative Type System. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.24,
  author =	{Guerrieri, Giulio and Heijltjes, Willem B. and Paulus, Joseph W.N.},
  title =	{{A Deep Quantitative Type System}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.24},
  URN =		{urn:nbn:de:0030-drops-134586},
  doi =		{10.4230/LIPIcs.CSL.2021.24},
  annote =	{Keywords: Lambda-calculus, Deep inference, Intersection types, Resource calculus}
}

Refine by Author
1 Guerrieri, Giulio
1 Heijltjes, Willem B.
1 Paulus, Joseph W.N.

Refine by Classification
1 Theory of computation → Lambda calculus
1 Theory of computation → Proof theory

Refine by Keyword
1 Deep inference
1 Intersection types
1 Lambda-calculus
1 Resource calculus

Refine by Type
1 document

Refine by Publication Year
1 2021

1 Search Results for "Paulus, Joseph W.N."

A Deep Quantitative Type System

Abstract

Cite as

Thanks for your feedback!

Could not send message