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.
Type de document :
Communication dans un congrès
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01091560
Contributeur : Ugo Dal Lago <>
Soumis le : vendredi 5 décembre 2014 - 16:07:25
Dernière modification le : samedi 27 janvier 2018 - 01:31:34
Document(s) archivé(s) le : samedi 15 avril 2017 - 04:06:50

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | PPS | USPC

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〉

Partager

Métriques

Consultations de la notice

275

Téléchargements de fichiers

199