tobast/L3-internship-report
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Few more lines

Browse source
This commit is contained in:
Théophile Bastian 2016-08-09 20:30:22 +01:00
parent e659c053a4
commit 15de66b6a5
2 changed files with 14 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
concurgames.sty
View file

@ -36,6 +36,7 @@
% LCCS
\newcommand{\lcalc}{$\lambda$-calculus}
\newcommand{\lccs}{$\lambda$CCS}
\newcommand{\llccs}{$\lambda$CCS$_\linarrow$}
\newcommand{\proc}{\mathbb{P}}

20
report.tex
View file

@ -36,7 +36,7 @@
\section{Introduction}
\paragraph{Game semantics} are a kind of operational semantics in which a
\paragraph{Game semantics} are a kind of denotational semantics in which a
program's behavior is abstracted as a two-players game, in which Player plays
for the program and Opponent plays for the environment of the program (the
user, the operating system, \ldots). The execution of a program, in this
@ -70,12 +70,12 @@ the two strategies.
\paragraph{Concurrency in game semantics.} In the continuity of the efforts put
forward to model imperative primitives in game semantics, it was natural to
focus at some point on modelling concurrency. The problem was tackled by
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a
$\lambda$-calculus with a few additions, as well as a \emph{parallel execution}
operator and communication on channels. It is often considered, though, that
\fname{Ghica} and \fname{Murawski}~\cite{ghica2004angelic} laid the first stone
by defining game semantics for a fine-grained concurrent language including
parallel execution of ``threads'' and low-level semaphores.
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{}
with a few additions, as well as a \emph{parallel execution} operator and
communication on channels. It is often considered, though, that \fname{Ghica}
and \fname{Murawski}~\cite{ghica2004angelic} laid the first stone by defining
game semantics for a fine-grained concurrent language including parallel
execution of ``threads'' and low-level semaphores.
However, both of these constructions are based on \emph{interleavings}. That
is, they model programs on \emph{tree-like games}, games in which the moves
@ -114,6 +114,12 @@ could not be reached --- but is not so far away ---, we have proved the
obtained an implementation of the (denotational) game semantics, that is, code
that translates a term of the language into its corresponding strategy.
\section{A linear \lcalc{} with concurrency primitives: \llccs}
\subsection{A linear variant of CCS}
\subsection{Lifting to the higher order: linear \lcalc}
\section{Existing work}
My work is set in the context of a wider theory, the basics of which are