[Prev][Next][Index][Thread]
paper on geometry of interaction
Date: Tue, 18 Feb 92 17:14:53 +0000
The following paper is now available by anonymous ftp from theory.doc.ic.ac.uk (in
papers/Abramsky). Anyone needing a hard copy should contact me.
Samson Abramsky
-------------
\documentstyle[11pt]{article}
\setlength{\oddsidemargin}{-0.3in}
\setlength{\textwidth}{6.7in}
\setlength{\topmargin}{-.25in}
\setlength{\textheight}{9.5in}
\headheight 0 pt
\headsep 0 pt
% Input macros if you have any.
% \changespacing allows you to redefine spacing commands.
\begin{document}
\title{ New foundations for the Geometry of Interaction\vspace{-8mm} }
\author{\parbox[t]{2in}{\begin{center} Samson Abramsky \\
Imperial College, \\
London.\\
\end{center}} \parbox[t]{2in}{\begin{center} Radha Jagadeesan \\
Imperial College, \\
London. \\
\end{center}}}\vspace{-5mm}
\date{}
\maketitle
\begin{abstract}
Girard has proposed the programme of Geometry of Interaction,
which aims to to find a new middle ground between
denotational and operational semantics, capturing the essential features of
computational dynamics in a syntax-free fashion using denotational tools.
He has implemented this programme using the formalism of
$C^{\star}$-algebras.
In this paper, we present a new formal embodiment of Girard's programme,
with the following salient features:
\begin{enumerate}
\item Our formalisation is based on Domain Theory, rather
than $C^{\star}$-algebras. We replace Girard's ``execution formula'' by a
least fixpoint, essentially a generalisation of Kahn's semantics for
feedback in dataflow networks. Coupled with the use of the other distinctive
construct of Domain theory, the lifting monad, this enables us to interpret the
whole of Classical Linear Logic, and to prove soundness in full generality,
thus addressing the technical limitations of Girard's formalisation.
\item We give a concrete computational interpretation of the Geometry of
Interaction in terms of dataflow networks.
\item We show how the interpretation
arises from the construction of a categorical model of Linear Logic, and
identify exactly what structure is required of the ambient category in
order to carry out the interpretation. This makes the definition of the
interpretation much more transparent.
\end{enumerate}
\end{abstract}
\end{document}