Parallelism and Synchronization in an Infinitary Context

Abstract : We study multitoken interaction machines in the context of a very expressive linear logical system with expo-nentials, fixpoints and synchronization. The advantage of such machines is to provide models in the style of the Geometry of Interaction, i.e., an interactive semantics which is close to low-level implementation. On the one hand, we prove that despite the inherent complexity of the framework, interaction is guaranteed to be deadlock-free. On the other hand, the resulting logical system is powerful enough to embed PCF and to adequately model its behaviour, both when call-by-name and when call-by-value evaluation are considered. This is not the case for single-token stateless interactive machines.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01231813
Contributor : Ugo Dal Lago <>
Submitted on : Friday, November 20, 2015 - 5:11:43 PM
Last modification on : Friday, January 4, 2019 - 5:32:59 PM
Long-term archiving on : Friday, April 28, 2017 - 6:36:51 PM

File

main_lics.pdf
Files produced by the author(s)

Identifiers

Citation

Ugo Dal Lago, Claudia Faggian, Benoît Valiron, Akira Yoshimizu. Parallelism and Synchronization in an Infinitary Context. LICS 2015, Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.58⟩. ⟨hal-01231813⟩

Share

Metrics

Record views

662

Files downloads

137