A polynomial time {\lambda}-calculus with multithreading and side effects
| Autor: | Madet, Antoine |
|---|---|
| Rok vydání: | 2012 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | The framework of Light Logics has been extensively studied to control the complexity of higher-order functional programs. We propose an extension of this framework to multithreaded programs with side effects, focusing on the case of polynomial time. After introducing a modal \lambda-calculus with parallel composition and regions, we prove that a realistic call-by-value evaluation strategy can be computed in polynomial time for a class of well-formed programs. The result relies on the simulation of call-by-value by a polynomial shallow-first strategy which preserves the evaluation order of side effects. Then, we provide a polynomial type system that guarantees that well-typed programs do not go wrong. Finally, we illustrate the expressivity of the type system by giving a programming example of concurrent iteration producing side effects over an inductive data structure. Comment: PPDP, Leuven : Belgique (2012) |
| Databáze: | arXiv |
| Externí odkaz: |
|