[logic-ml] Talk by Gabriele Vanoni (July 18th, 11.00-)

[Kazushige TERUI]

みなさま

今週木曜に京都大学にて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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.fos.kuis.kyoto-u.ac.jp/pipermail/logic-ml/attachments/20190714/88e1e0ba/attachment.html>