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.