Skip to Main content Skip to Navigation
Conference papers

Quantitative Types for the Linear Substitution Calculus

Abstract : We define two non-idempotent intersection type systems for the linear substitution calculus, a calculus with partial substitutions acting at a distance that is a computational interpretation of linear logic proof-nets. The calculus naturally express linear-head reduction, a notion of evaluation of proof nets that is strongly related to abstract machines. We show that our first (resp. second) quantitave type system characterizes linear-head, head and weak (resp. strong) normalizing sets of terms. All such characterizations are given by means of combinatorial arguments, i.e. there is a measure based on type derivations which decreases with respect to each reduction relation considered in the paper.
Document type :
Conference papers
Complete list of metadata

Cited literature [40 references]  Display  Hide  Download

https://hal.inria.fr/hal-01402078
Contributor : Hal Ifip <>
Submitted on : Thursday, November 24, 2016 - 11:08:59 AM
Last modification on : Friday, March 27, 2020 - 3:59:15 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 4:36:29 AM

File

978-3-662-44602-7_23_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Delia Kesner, Daniel Ventura. Quantitative Types for the Linear Substitution Calculus. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.296-310, ⟨10.1007/978-3-662-44602-7_23⟩. ⟨hal-01402078⟩

Share

Metrics

Record views

358

Files downloads

848