Ulrich Schöpp: The Geometry of Interaction as a Module System
Es spricht Ulrich Schöpp über:
The Geometry of Interaction as a Module System
Abstract:
The Geometry of Interaction (GoI) was originally introduced by Girard
in the context of Linear Logic. A number of its recent applications
concern the interpretation and analysis of functional programming
languages, with applications ranging from hardware synthesis to
quantum computation. In this talk I will argue that for such
programming-language applications it is useful to understand the GoI
as a module system in the style of Standard ML. The structure of
particle-style GoI models is naturally expressed by such a module
system. This view provides a familiar formalism for working with the
GoI that abstracts from inessential implementation details and that is
convenient for implementation tasks. With this view, the GoI becomes
a method of implementing ML-style module systems for a wide range of
first-order programming languages. It can be considered as a
higher-order generalisation of systems-level linking. The relation
between the GoI and the proposed module system is established by a
linear version of the F-ing modules approach of Rossberg, Russo and
Dreyer that uses as new decomposition of the exponential rules of
Linear Logic.
Artikelaktionen