An Elementary affine λ-calculus with multithreading and side effects (extended version) - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports Year : 2011

An Elementary affine λ-calculus with multithreading and side effects (extended version)

Roberto M. Amadio

Abstract

Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side effects focusing on the case of elementary time. Our main contributions are as follows. First, we provide a new combinatorial proof of termination in elementary time for the functional case. Second, we develop an extension of the approach to a call-by-value $lambda$-calculus with multithreading and side effects. Third, we introduce an elementary affine type system that guarantees the standard subject reduction and progress properties. Finally, we illustrate the programming of iterative functions with side effects in the presented formalism.
Fichier principal
Vignette du fichier
rapport.pdf (348.18 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00569095 , version 1 (24-02-2011)
hal-00569095 , version 2 (10-06-2011)

Identifiers

Cite

Antoine Madet, Roberto M. Amadio. An Elementary affine λ-calculus with multithreading and side effects (extended version). 2011. ⟨hal-00569095v2⟩
816 View
123 Download

Altmetric

Share

Gmail Facebook X LinkedIn More