The Geometry of Synchronization

Abstract : We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplica-tive linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Inter-estingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/hal-01091560
Contributor : Ugo Dal Lago <>
Submitted on : Friday, December 5, 2014 - 4:07:25 PM
Last modification on : Friday, January 4, 2019 - 5:32:59 PM
Long-term archiving on : Saturday, April 15, 2017 - 4:06:50 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, Akira Yoshimizu. The Geometry of Synchronization. Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603154⟩. ⟨hal-01091560⟩

Share

Metrics

Record views

583

Files downloads

310