Name
Abstract | ||
|---|---|---|
We characterize β-strongly normalizing λ-terms by means of a non-idempotent intersection type system. More precisely, we first define a memory calculus K together with a non-idempotent intersection type system K, and we show that a K-term t is typable in K if and only if t is K-strongly normalizing. We then show that β-strong normalization is equivalent to K-strong normalization. We conclude since λ-terms are strictly included in K-terms. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1016/j.entcs.2016.06.006 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
Lambda-calculus,memory calculus,strong normalization,intersection types | Discrete mathematics,Lambda calculus,Normalization (statistics),If and only if,Normalization property,Mathematics | Journal |
Volume | Issue | ISSN |
323 | C | 1571-0661 |
Citations | PageRank | References |
0 | 0.34 | 17 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Antonio Bucciarelli | 1 | 241 | 25.59 |
| Delia Kesner | 2 | 369 | 39.75 |
| Daniel Lima Ventura | 3 | 22 | 4.88 |