Name
Abstract | ||
|---|---|---|
Inspired by the Multiplicative Exponential fragment of Linear Logic, we define a framework called the prismoid of resources where each vertex is a language which refines the @l-calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of @b-reduction, confluence, preservation of @b-strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter of the formalism, so that all the properties for each vertex are obtained as a particular case of the general abstract proofs. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1016/j.tcs.2011.01.026 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
full composition,Lambda-calculus,particular case,substitution operation,Linear Logic,Multiplicative Exponential fragment,prismoid framework,strong normalisation,Explicit resources,b-strong normalisation,different choice,general abstract proof,explicit substitution | Journal | 412 |
Issue | ISSN | Citations |
37 | Theoretical Computer Science | 5 |
PageRank | References | Authors |
0.42 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Delia Kesner | 1 | 369 | 39.75 |
| Fabien Renaud | 2 | 30 | 2.47 |