みなさま

今週木曜に京都大学にてGabriele Vanoniさんによるご講演があります。 詳細は下記の通りです。よろしければご参加ください。

京都大学数理解析研究所 照井一成

========== Time: 11:00-12:00, July 18th, 2019 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34)

Speaker: Gabriele Vanoni (Univ. Bologna)

Title: The Geometry of Abstract Machines

Joint work with Ugo Dal Lago and Beniamino Accattoli

Geometry of Interaction (GOI) is a semantic framework describing the dynamics of cut-elimination in the Multiplicative Exponential fragment of Linear Logic (MELL). It has been formulated in many ways, from operator algebras to traced symmetrical monoidal categories. Remarkably, some of these formulations, in particular Context Semantics by Gonthier et al. led to the introduction of compilation techniques (Mackie '95) and abstract machines for higher-order functional languages (Danos and Regnier '99). However, these machines were always based on a proof-net representation of programs, via the so-called Girard translation. We introduce an abstract machine in the spirit of GOI based directly on the λ-calculus, without any explicit use of proof-nets. We prove soundness and adequacy, and we derive in our framework an optimization already presented by Danos and Regnier. We intend to analyze in the future the complexity of these machines, with particular emphasis on the trade-off between space and time efficiency.