2014/05/14 by Ugo Dal Lago, Lago, Ugo Dal, Claudia Faggian +5
Computer Science · #F.3.2 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1405.3427
26 pages
arxiv created 2014/05/14 · arxiv updated 2014/05/15
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 multiplicative linear logic with a specific construct modeling synchronization points, and of a multi-token abstract machine model for it. Interestingly, the correctness criterion ensures the absence of deadlocks along reduction and in the underlying machine, this way linking logical and operational properties.