<div dir="ltr">みなさま<br><br>今週木曜に京都大学にてGabriele Vanoniさんによるご講演があります。<br>詳細は下記の通りです。よろしければご参加ください。<br><br>京都大学数理解析研究所<br>照井一成<br><br>==========<br>Time:    11:00-12:00, July 18th, 2019<br>Place:    Rm 478, Research Building 2, Main Campus, Kyoto University<br>    京都大学 本部構内 総合研究2号館 4階478号室<br>    <a href="http://www.kyoto-u.ac.jp/en/access/yoshida/main.html">http://www.kyoto-u.ac.jp/en/access/yoshida/main.html</a> (Building 34)<br><br>Speaker: Gabriele Vanoni (Univ. Bologna) <br><br>Title: The Geometry of Abstract Machines<br><br>Joint work with Ugo Dal Lago and Beniamino Accattoli<br><br>Geometry of Interaction (GOI) is a semantic framework describing<br>the dynamics of cut-elimination in the Multiplicative Exponential<br>fragment of Linear Logic (MELL). It has been formulated in many ways, from<br>operator algebras to traced symmetrical monoidal categories. Remarkably, some of<br>these formulations, in particular Context Semantics by Gonthier et al. led to<br>the introduction of compilation techniques (Mackie '95) and abstract machines for<br>higher-order functional languages (Danos and Regnier '99). However, these machines<br>were always based on a proof-net representation of programs, via the so-called<br>Girard translation. We introduce an abstract machine in the spirit of GOI based<br>directly on the λ-calculus, without any explicit use of proof-nets. We prove<br>soundness and adequacy, and we derive in our framework an optimization already<br>presented by Danos and Regnier. We intend to analyze in the future the<br>complexity of these machines, with particular emphasis on the trade-off between<br>space and time efficiency.<br></div>