Loading...
Please wait, while we are loading the content...
Similar Documents
Translating types and effects with state monads and linear logic
| Content Provider | Semantic Scholar |
|---|---|
| Author | Tranquilli, Paolo |
| Copyright Year | 2010 |
| Abstract | We study a lambda-calculus with references and a types and effects system. In the first part of the paper, we translate it into the ordinary lambda-calculus with products, implementing an interacting family of state monads localized at sets of regions. In general the target language must be endowed with recursive types. However we prove that the stratification condition on regions, already used in type and effect systems to assure termination, is equivalent to completely avoid the use of recursion in the types used in the translation. We thus obtain a logical characterization of stratification, and by simulation we also provide a new proof that it yields termination. In the second part of the paper we extend the call-by-value translation of ordinary lambda-terms in linear logic proof nets to the calculus with references. This allows for a parallel evaluation of the calculus that preserves its sequential semantics. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://hal-ens-lyon.archives-ouvertes.fr/docs/00/46/57/93/PDF/typeseffects.pdf |
| Alternate Webpage(s) | http://hal.archives-ouvertes.fr/docs/00/46/57/93/PDF/typeseffects.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
