%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Ne rien modifier dans les déclarations qui suivent.
% Tout cette partie sera ignorée dans la compilation globale.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\ifundefined#1{\expandafter\ifx\csname#1\endcsname\relax}
\ifundefined{MPRIglobal}
\documentclass[11pt,a4paper]{article}
% \usepackage[applemac]{inputenc}
\usepackage[latin1]{inputenc}
\usepackage[french]{babel}

\textheight=227mm  
\textwidth=160mm 
 
\topmargin=297mm
\advance \topmargin by -\textheight 
\divide  \topmargin by 2
\advance \topmargin by -1in 
\advance \topmargin by -\headheight
\advance \topmargin by -\headsep

\leftmargin=210mm
\advance \leftmargin by -\textwidth 
\divide  \leftmargin by 2
\advance \leftmargin by -1in 

\oddsidemargin=\leftmargin
\evensidemargin=\leftmargin 

\parskip=4pt
\pagestyle{plain}

\newcounter{bibliocpt}
\newenvironment{mabiblio}[1]%
  {\begin{list}{\addtocounter{bibliocpt}{1}[\arabic{enumiv}]}{
    \usecounter{enumiv}\setcounter{enumiv}{\value{bibliocpt}}
    \renewcommand{\makelabel}[1]{##1\hfil}
    \settowidth{\labelwidth}{#1}
    \setlength{\leftmargin}{\labelwidth}
    \addtolength{\leftmargin}{\labelsep}}}
  {\end{list}}

\renewcommand{\paragraph}[1]{\par\bigskip\noindent\textbf{\large #1}\par\medskip}

\begin{document}
\begin{sloppypar}

\appendix
~
\vfill
\section{Descriptif des cours de niveau 2} \label{annexe:cours-de-niveau-2}
\vfill
~
\fi
\setcounter{bibliocpt}{0}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Ne rien modifier dans les déclarations ci-dessus.
% Tout ce qui précède sera ignoré dans la compilation globale.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% MAXIMUM 2 PAGES POUR LA FICHE D'UN COURS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Concurrence (C-2-03)}
\label{C-2-03} % numér\item du cours. par exemple C-1-03, C-2-04-1, ...

%%%%%%%%%%
\paragraph{Responsables}
Catuscia Palamidessi (INRIA Futurs), Roberto Amadio (PPS, Paris 7) 
et Jean-Jacques Levy (INRIA Rocquencourt).

%%%%%%%%%%
\paragraph{Motivations et objectifs du cours}
% Description en quelques lignes du contexte du cours et de ses principaux
% objectifs

Ce cours est une introduction aux calculs de processus, c'est-à-dire à des systèmes formels qui permettent de raisonner sur les propriétés des programmes concurrents et possiblement répartis.

Les calculs de processus représentent à un niveau abstrait la création et l'exécution de processus et leurs mécanismes de synchronisation élémentaire: mémoire partagée, communication par canaux, etc. Ces calculs élémentaires sont, pour les processus concurrents, l'analogue du lambda calcul pour les programmes séquentiels.

Pendant le cours, nous donnerons des exemples d'application de ces formalismes à la conception de langages de programmation et à la spécification et vérification de systèmes répartis. Nous montrerons en outre quelques exemples récents de leur utilisation dans le traitement formel de problèmes de sécurité. 


%%%%%%%%%%
\paragraph{Plan du cours}
% Plan plus détaillé de ce qui va être enseigné, sans que cela soit
% contractuel.  Il n'est pas nécessaire d'indiquer des volumes horaires
% pour les différents cours, ni les intervenants précis pour chaque partie

\begin{enumerate}
  \item Introduction et motivations (1h)

    \item Calcul des Systèmes Communicants (CCS) (11h)
          \begin{itemize}
          \item Syntaxe
          \item Sémantique Opérationnelle (SOS)
          \item Arbres de Synchronisation
          \item Traces
          \item Bisimulation Forte
          \item Bisimulation Faible
          \item Théorie de l'Egalité
          \item Logique Hennessy-Milner
          \item Model Checking
          \item Exemples de spécification et vérification en CCS
          \end{itemize}

    \item Le $\pi$-calcul (9h)
          \begin{itemize}
          \item Syntaxe
          \item Sémantique late et early
          \item Le $\pi$-calcul asynchrone
          \item Types
          \item Théorie de l'égalité
          \item Exemples de spécifications dans le $\pi$-calcul
          \item Autres approches à la mobilité
          \end{itemize}

    \item Calculs de processus probabilistes et applications (15h)
          \begin{itemize}
          \item Expressivité des calculs. Rôle de la randomisation.
          \item Automates probabilistes et calculs de processus probabilistes.
          \item Application : solution randomisée de problèmes d'algorithmique répartie.
          \item Application: Confidentialité et Anonymat.
          \end{itemize}

    \item Notions avancées (12h)
          \begin{itemize}
          \item Déterminisme et Confluence.
          \item Synchronie.
          \item Types et Ressources en Concurrence.
          \item Application à l'analyse du Flot d'Information 
          \end{itemize}

\end{enumerate}


%%%%%%%%%%
\paragraph{Pré-requis}
% Partie facultative si aucun pré-requis spécifique n'est attendu

Pas de pré-requis.

%%%%%%%%%%
\paragraph{Bibliographie}
% Quelques points d'entrée de la bibliographie permettant de se faire une
% idée plus précise du cours

\begin{mabiblio}{10}
  \bibitem{Mil89}
  Robin Milner
  \newblock {\em Communication and Concurrency}.
  \newblock International Series in Computer Science. Prentice Hall, 1989.

  \bibitem{Mil99}
  Robin Milner.
  \newblock {\em The $\pi$-calculus}.
  \newblock Cambridge University Press, 1999.

  \bibitem{ManPnu91}
  Davide Sangiorgi and David Walker.
  \newblock {\em The $\pi$-calculus: a Theory of Mobile Processes}.
  \newblock Springer, 1991.

\end{mabiblio}
\unskip

%%%%%%%%%%
\paragraph{Intervenants possibles}
% Merci de respecter le format en indiquant le grade (MC, PR, CR, DR,...)
% l'établissement d'affectation et le laboratoire de recherche selon les
% modèles ci-dessous. Tous les tableaux seront fusionnés 

\begin{tabular}{|l|c|l|l|}
  \hline
  Nom & Grade 	& Établissement & Laboratoire % & Cours 
  \\ \hline
  R. Amadio    	& PR & Paris 7 	& PPS 
  \\ \hline
  P.-L. Curien 	& PR & Paris 7 	& PPS 
  \\ \hline
  E. Goubault	& DR & CEA     	& Saclay 
  \\ \hline
  J.-J. L\'evy 	& DR & INRIA  	& Rocquencourt 
  \\ \hline
  J. Leifer  	& CR & INRIA  	& Rocquencourt 
  \\ \hline
  C. Palamidessi& DR & INRIA   	& Futurs 
  \\ \hline
  F. Valencia 	& CR & Paris 7  & PPS 
  \\ \hline
  F. Zappa Nardelli & CR & INRIA      & Rocquencourt 
  \\ \hline
\end{tabular}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ifundefined{MPRIglobal}
\end{sloppypar}
\end{document}
\fi
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
