Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, November 24, 2016 - 11:08:59 AM
Last modification on : Saturday, June 25, 2022 - 8:57:44 PM
Long-term archiving on: : Tuesday, March 21, 2017 - 4:36:29 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads