Paper Info
Title
A resource aware semantics for a focused intuitionistic calculus.
Abstract
We investigate a new computational interpretation for an intuitionistic focused sequent calculus which is compatible with a resource aware semantics. For that, we associate to Herbelin's syntax a type system based on non-idempotent intersection types, together with a set of reduction rules - inspired from the substitution at a distance paradigm - that preserves (and decreases the size of) typing derivations. The non-idempotent approach allows us to use very simple combinatorial arguments, only based on this measure decreasingness, to characterize linear-head and strongly normalizing terms by means of typability. For the sake of completeness, we also study typability (and the corresponding strong normalization characterization) in the calculus obtained from the former one by projecting the explicit cuts.
Year
DOI
Venue
2019
10.1017/S0960129517000111
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE
Field
DocType
Volume
Discrete mathematics,Operational semantics,Semantics,Mathematics,Calculus
Journal
29
Issue
ISSN
Citations 
SP1
0960-1295
0
PageRank 
References 
Authors
0.34
12
2
Name
Order
Citations
PageRank
Delia Kesner136939.75
Daniel Lima Ventura2224.88