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. © 2014 IFIP International Federation for Information Processing.
CITATION STYLE
Kesner, D., & Ventura, D. (2014). Quantitative types for the linear substitution calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8705 LNCS, pp. 296–310). Springer Verlag. https://doi.org/10.1007/978-3-662-44602-7_23
Mendeley helps you to discover research relevant for your work.