%% Time-stamp: <modified on 16 Sep 2004 at 15:04 by Pierre Lescanne>
%% intro_sem.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
\usepackage{epsfig}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}


\input{macros}

\slidesmag{5}
\articlemag{1}


\title{\color{red}{\textit{Introduction}}}

\author{}

\date{}

\newcommand{\logoLIP}{\includegraphics*[height=0.04\textwidth]{lipllipl.eps}}
\newcommand{\logoENS}{\includegraphics*[height=0.04\textwidth]{liplensl.eps}}
\newcommand{\logos}{\hspace*{6pt}WPI --- September 2002 \hfill\logoLIP\hspace*{6pt}\logoENS}


\newpagestyle{AvecLogos}%
  {\tiny \em introduction de la sémantique -- \jour 
  \hfil \thepage} % \rightmark
  {\logos}
%\pagestyle{AvecLogos}

\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\input{mes_couleurs}

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{\ra}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\envdot}{\bullet}
\newcommand{\cm}[2]{\langle #1 \parallel #2\rangle}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\perluette}{&}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                les symboles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Lift}{\Uparrow\!\!}
\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                headings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255

\newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,:\,
   \ifnum\timemm<10 0\fi\number\timemm}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}
%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%%------------------------------------------------------
%\begin{slide}
%  \begin{center}
%    {\large \bf \color{green}{\textit{}}}
%\end{center}
%\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Qu'est-ce que la sémantique? }

 \emph{Sémantique}: \textit{Étude du sens, de la signification dans le langage.}
 \rightline{Dictionnaire Robert.}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Pourquoi la sémantique? 1/2}%
Définir la sémantique d'un langage formel consiste à lui donner une
signification mathématique, dans deux buts.
\begin{description}
\item[\emph{La description},] qui doit permettre de cerner très précisément ce que
  réalise un programme (ou un circuit) 
  \begin{itemize}
  \item afin de permettre au programmeur de comprendre ce qu'il fait,
    
  \item afin de réaliser des traducteurs (compilateurs, interprètes)
    et des optimiseurs,
  \item afin de pouvoir appliquer des méthodes formelles de vérification,
  \end{itemize}
  \vfill
\end{description}
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Pourquoi la sémantique? 2/2}%
\begin{description}
\item[\emph{La prescription},] {\footnotesize (dans les sens du verbe
    \verdir{prescrire})} qui doit aider les concepteurs de langages à
  définir des langages cohérents, puissants et corrects, (qui se
  souvient du monstre PL/1?).  Ceci est très important avec la
  définition des \emph{langages de domaines spécifiques}, par exemple
  \begin{itemize}
  \item un langage pour aider les ingénieurs à calculer les
    trajectoires des satellites,
  \item un langage pour commander un micro-onde lors de la cuisson d'un
    plat surgelé.
  \end{itemize}
\end{description}

\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Un concept de sémantique: la transparence référentielle 1/3}%
La sémantique a mis en évidence un concept important: \ali la
\emph{transparence référentielle}.

Un langage formel est \emph{référentiellement transparent} si, dans la
même portée, la signification d'une portion de code est indépendante de
sa position dans le code.

\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Un concept de sémantique: la transparence référentielle 2/3}%
Ainsi CAML n'est pas référentiellement transparent.

On s'attend à ce que pour chaque invocation \ali de \texttt{(f 1) * (f
  1) - (f 1) * (f 1)} dans
\begin{verbatim}
(f 1) * (f 1) - (f 1) * (f 1);;
(f 1) * (f 1) - (f 1) * (f 1);;
(f 1) * (f 1) - (f 1) * (f 1);;
(f 1) * (f 1) - (f 1) * (f 1);;
(f 1) * (f 1) - (f 1) * (f 1);;
\end{verbatim}
on obtienne la valeur 0.
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Un concept de sémantique: la transparence référentielle 3/3}%
 Mais en fait on obtient successivement
\texttt {14, 30, 46, 62, 78} si on définit \texttt{f} par 
\begin{verbatim}
let r = ref 0;;
 let f x = (r:=!r+1; x + !r);;
\end{verbatim}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Les types de sémantique}%
\begin{description}
\item[\emph{opérationnelle},] on définit la sémantique par
  sa mise en {\oe}uvre sur une machine abstraite (ou quelque chose qui
  lui ressemble comme un système de réduction), on distingue
  \begin{footnotesize}
  \begin{itemize}
  \item la \verdir{sémantique en grandes étapes}, qui associe au
    programme une transition données-résultats,
  \item la \verdir{sémantique en petites étapes}, qui décrit le
    comportement du programme étape par étape,
  \end{itemize}
\end{footnotesize}
\item[\emph{dénotationnelle},] on associe à chaque construction
  syntaxique un objet mathématique qui est défini par récurrence sur
  la structure
\item[\emph{axiomatique},] chaque construction est décrite par la
  manière dont elle transforme des propriétés ou des prédicats.
\end{description}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Et la syntaxe dans tout ça ?}%

\vspace*{20pt}

\fbox{\parbox{8cm}{
 \textit{ «La sémantique n'a rien à faire du sucre syntaxique.»}
\rightline{d'après Christoffer Strachey}}}


\vspace*{20pt}

La sémantique suppose que tout le travail d'analyse syntaxique est fait.

Elle travaille au niveau de la syntaxe abstraite : objet structuré
et/ou arborescent construit à partir de l'arbre d'analyse syntaxique,
lui-même construit à partir du texte linéaire du programme.

\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le plan (provisoire) du cours 1/2}%
\begin{footnotesize}
\begin{math}
\left.
\parbox{5.5cm}{
 \begin{itemize}
 \item[$\bullet$] La sémantique d'un langage impératif,
  \begin{itemize}
  \item la sémantique opérationnelle,
  \item la sémantique dénotationnelle,
  \item la sémantique axiomatique
  \end{itemize}
\end{itemize}
}
\right\}  
\end{math}\parbox{3cm}{\emph{Le but est d'étudier un cas particulier}}
\end{footnotesize}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le plan (provisoire) du cours 2/2}%
\begin{footnotesize}
\begin{math}
\left.
\parbox{6cm}{
\begin{itemize}
\item[$\bullet$] La sémantique du lambda calcul,
  \begin{itemize}
  \item la sémantique opérationnelle,
    \begin{itemize}
    \item les substitutions explicites,
    \item la sémantique à grandes étapes,
    \item les machines abstraites,
    \item le style de passages de continuations,
   \item les réseaux d'interaction de Lamping,
    \end{itemize}
 \item la sémantique dénotationnelle,
   \begin{itemize}
   \item les modèles par retracts,
   \item le modèle de Scott
   \end{itemize}
 \item La cohérence du calcul typée par forte normalisation: le cas du
   système \textsf{F};
 \end{itemize}
\end{itemize}
}
\right\}  
\end{math}\parbox{3cm}{\emph{Le but est d'introduire des concepts}}
\end{footnotesize}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Quelques livres}%

\brunir{Glynn Winskel},  \verdir{Formal semantics of programming language},
  \ali MIT Press 	 (1993).

  \brunir{John Mitchell}, \verdir{Concepts in programming
    languages}, \ali Cambridge University Press (2003).


  \brunir{John Mitchell}, \verdir{Foundations for Programming
    Languages}, \ali MIT Press, (1996).


  \brunir {R. M. Amadio and P.-L. Curien}, \verdir{Domains and
    Lambda-calculi}, \ali {Cambridge University Press}, (1998).

\vfill
\end{slide}
%%----------------------------------------------------------------------
%\begin{slide}
%\heading{Le plan (provisoire) du cours 3/3}%
%\begin{small}
%\begin{itemize}
%\item[$\bullet$] L'exercursion de nouvaux 
%  \emph{Un modèle important}
%\end{itemize}
%\end{small}
%\vfill
%\end{slide}
\end{document}
% LocalWords:  optimiseurs prescriptif PL référentiellement Lamping retracts
% LocalWords:  Scott
