Back to Search
Start Over
A Deep Quantitative Type System
- Source :
- Guerrieri, G, Heijltjes, W & Paulus, J 2021, A deep quantitative type system . in C Baier & J Goubault-Larrecq (eds), 29th EACSL Annual Conference on Computer Science Logic, CSL 2021 : CSL 2021 . 2021 edn, vol. 183, 24, Leibniz International Proceedings in Informatics, LIPIcs, vol. 183, Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Dagstuhl, Germany, pp. 24:1-24:24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Lubijana, Slovenia, 25/01/21 . https://doi.org/10.4230/LIPIcs.CSL.2021.24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), 24:1-24:24, STARTPAGE=24:1;ENDPAGE=24:24;TITLE=29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
- Publication Year :
- 2021
- Publisher :
- Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 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.<br />LIPIcs, Vol. 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 24:1-24:24
- Subjects :
- TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Deep inference
Theory of computation → Proof theory
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
Theory of computation → Lambda calculus
Lambda-calculus
Intersection types
Software
Resource calculus
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Journal :
- Guerrieri, G, Heijltjes, W & Paulus, J 2021, A deep quantitative type system . in C Baier & J Goubault-Larrecq (eds), 29th EACSL Annual Conference on Computer Science Logic, CSL 2021 : CSL 2021 . 2021 edn, vol. 183, 24, Leibniz International Proceedings in Informatics, LIPIcs, vol. 183, Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Dagstuhl, Germany, pp. 24:1-24:24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Lubijana, Slovenia, 25/01/21 . https://doi.org/10.4230/LIPIcs.CSL.2021.24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), 24:1-24:24, STARTPAGE=24:1;ENDPAGE=24:24;TITLE=29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
- Accession number :
- edsair.doi.dedup.....fd66c817ee971ec5d3c66094f45a2541