Name
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 strongly normalizing terms by means of typability. For the sake of completeness, we also study typability and the corresponding strong normalization characterization in the reduction calculus obtained from the former one by projecting the explicit substitutions. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-25150-9_23 | ICTAC |
Field | DocType | Volume |
Discrete mathematics,Normalization (statistics),Computer science,Sequent calculus,Theoretical computer science,Syntax,Completeness (statistics),Semantics | Conference | 9399 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.40 |
References | Authors | |
18 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Delia Kesner | 1 | 369 | 39.75 |
| Daniel Lima Ventura | 2 | 22 | 4.88 |