24 citations · 27 across the 4 of their papers we have counts for
6 papers
Differential Logical Relations, Part I: The Simply-Typed Case (Long Version)
Ugo Dal Lago, Francesco Gavazzo, Akira Yoshimizu
We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a b…
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
Yosuke Fukuda, Akira Yoshimizu
We propose a "modal linear logic" to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. Whil…
The Geometry of Concurrent Interaction: Handling Multiple Ports by Way of Multiple Tokens (Long Version)
Ugo Dal Lago, Ryo Tanaka, Akira Yoshimizu
We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation a…
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
Ugo Dal Lago, Claudia Faggian, Benoit Valiron +1
We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication…
Parallelism and Synchronization in an Infinitary Context (Long Version)
Ugo Dal Lago, Claudia Faggian, Benoit Valiron +1
We study multitoken interaction machines in the context of a very expressive logical system with exponentials, fixpoints and synchronization. The advantage of such machines is to p…
The Geometry of Synchronization (Long Version)
Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo +1
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 o…