\documentclass[pdf,nototal,rico,slideColor,colorBG]{prosper}

%\usepackage{pstricks,pst-node,pst-text,pst-3d}
\usepackage{amsmath}
\usepackage{alltt}

\usepackage{colordvi}
\usepackage{proof}
\usepackage{epsf}
\usepackage{amssymb}
\usepackage{a4}

\usepackage{epsfig}

\newcommand{\tab}{\null\hskip1cm}
\newcommand{\colbox}[2]{\textcolor{#1}{\framebox{\textcolor{black}{\(#2\)}}}}
\newcommand{\prop}{\mathbf{Prop}}
\newcommand{\set}{\mathbf{Set}}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\bool}{\mathbb{B}}
 
\newcommand{\com}{\mathsf{Command}}
\newcommand{\state}{\mathsf{State}}
\newcommand{\aexp}{\mathsf{AExp}}
\newcommand{\bexp}{\mathsf{BExp}}
 
\newcommand{\const}[1]{\mathsf{Num}(#1)}
\newcommand{\loc}[1]{\mathsf{Loc}(#1)}
 
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
 
\newcommand{\skp}{\mathsf{skip}}
\newcommand{\assign}[2]{#1 \leftarrow #2}   %{#1:=#2}
\newcommand{\scolon}[2]{#1; #2}
\newcommand{\ifthenelse}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\
\mathsf{else}\ #3}
\newcommand{\whiledo}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
\newcommand{\exception}{\mathsf{exception}}
 
\newcommand{\noloc}{[]}
\newcommand{\oneloc}[3]{[#1 \mapsto #2,#3]}
 
\newcommand{\valueind}{\mathsf{value\_ind}}
\newcommand{\nosuchloc}{\mathsf{no\_such\_location}}
\newcommand{\firstloc}{\mathsf{first\_location}}
\newcommand{\restloc}{\mathsf{rest\_locations}}
\newcommand{\evalnum}{\mathsf{eval\_Num}}
\newcommand{\evalloc}{\mathsf{eval\_Loc}}
\newcommand{\evalplus}{\mathsf{eval\_Plus}}
\newcommand{\evalminus}{\mathsf{eval\_Minus}}
\newcommand{\evalmult}{\mathsf{eval\_Mult}}
 
\newcommand{\updatenoloc}{\mathsf{update\_no\_location}}
\newcommand{\updatefirst}{\mathsf{update\_first}}
\newcommand{\updaterest}{\mathsf{update\_rest}}
 
\newcommand{\opint}[3]{\langle #1, #2\rangle \leadsto #3}
\newcommand{\opinta}[3]{\langle #1, #2\rangle_\mathsf{A}\leadsto #3}
\newcommand{\opintb}[3]{\langle #1, #2\rangle_\mathsf{B}\leadsto #3}
\newcommand{\opintc}[3]{\langle #1, #2\rangle_\mathsf{C}\leadsto #3}
 
\newcommand{\updateind}[4]{{#1}_{[#2 \mapsto #3]} \leadsto #4}
 
\newcommand{\evalskip}{\mathsf{eval\_skip}}
\newcommand{\evalassign}{\mathsf{eval\_assign}}
\newcommand{\evalscolon}{\mathsf{eval\_scolon}}
\newcommand{\evaliftrue}{\mathsf{eval\_if\_true}}
\newcommand{\evaliffalse}{\mathsf{eval\_if\_false}}
\newcommand{\evalwhiletrue}{\mathsf{eval\_while\_true}}
\newcommand{\evalwhilefalse}{\mathsf{eval\_while\_false}}
 
\newcommand{\valuerec}[2]{\mathsf{value\_rec}(#1,#2)}
\newcommand{\interl}{[\![}
\newcommand{\interr}{]\!]}
\newcommand{\inter}[1]{\interl #1 \interr}
 
% \updaterec{s}{X}{a} updates the state s by assigning a to X
\newcommand{\updaterec}[3]{#1[#3/#2]}
 
\newcommand{\Fo}{\mathsf{F}}
\newcommand{\evalcomindrec}{\mathsf{eval\_com\_ind\_to\_rec}}
\newcommand{\s}{\mathsf{S}}
\newcommand{\iter}{\mathsf{iter}}
\newcommand{\nobound}{\omega}
\newcommand{\fix}{\mathsf{fix}}
 
\newcommand{\Acc}{\mathsf{Acc}}
\newcommand{\comAcc}{\mathsf{comAcc}}
\newcommand{\accSkip}{\mathsf{accSkip}}
\newcommand{\accAssign}{\mathsf{accAssign}}
\newcommand{\accScolon}{\mathsf{accScolon}}
\newcommand{\accIftrue}{\mathsf{accIf\_true}}
\newcommand{\accIffalse}{\mathsf{accIf\_false}}
\newcommand{\accWhiletrue}{\mathsf{accWhile\_true}}
\newcommand{\accWhilefalse}{\mathsf{accWhile\_false}}
 
\newcommand{\evalcom}[3]{\inter{#1}_{#2}^{#3}}
\newcommand{\comdom}{\mathsf{comDom}}





\title{Type-theoretic functional semantics}
\subtitle{}
\author{Yves Bertot, \\
Venanzio Capretta, \\ 
Kuntal Das Barman
}

\institution{
  {\textsc{INRIA}} Sophia-Antipolis, France 
}
\email{FirstName.Surname@sophia.inria.fr}

\LogoPosition{-.6,7.6}
\Logo{\includegraphics[width=.8in]{./figures/Logo-INRIA-Sophia.ps}}

\date{TPHOLs 2002}


\begin{document}
\maketitle

%------------------------------------------------------

\overlays{7}{
\begin{slide}{How do we proceed?}
\footnotesize
\vspace{.2in}
\begin{itemstep}
\item A small imperative language - IMP
\item Operational semantics for IMP
\item Specification problem with denotational semantics and its solution
\item Assurance of termination and accessibility predicate
\item Solution in simultaneous induction-recursion
\item Disentangle simultaneous induction-recursion for Coq
\item Conclusion
\end{itemstep}
\end{slide}
}

%------------------------------------------------------

\overlays{4}{
\begin{slide}{IMP - a small imperative language}
\footnotesize
\vspace{.2in}
\begin{itemstep}
\item {\blue arithmetic expressions ($\aexp$)}\\
 $a::= n \mid X \mid a_0 + a_1 \mid a_0 - a_1 \mid a_0 * a_1$,
\item {\blue boolean expressions ($\bexp$)}\\
$b::= \true \mid \false \mid a_0 = a_1 \mid
a_0 \leq a_1 \mid \neg b \mid b_0 \vee b_1 \mid b_0 \wedge b_1$,
\item {\blue commands ($\com$)}\\
$c::= \skp \mid \assign{X}{a} \mid \scolon{c_0}{c_1} \mid
 \ifthenelse{b}{c_0}{c_1} \mid \whiledo{b}{c}$,
\item {\blue states ($\state$)}\\
 Keeps track of contents of locations($X$)
\end{itemstep}
\end{slide}
}

%------------------------------------------------------

\overlays{3}{
\begin{slide}{Evaluation}
\footnotesize
\begin{itemize}
\item[]
\item[]
\item \fromSlide{1}{{\blue Arithmetic Expressions} : \(\opinta{\aexp}{\state}{\mathtt{Natural\ \; Number}}\)}
\item[]
\item \fromSlide{2}{{\blue Boolean Expressions} : \ \ \ \(\opintb{\bexp}{\state}{\mathtt{Boolean\ \; Value}}\)}
\item[]
\item \fromSlide{3}{{\blue Commands} : \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \(\opintc{\com}{\state}{\mathtt{\state}}\)}
\end{itemize}
\vspace*{1in}
\end{slide}
}

%------------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\red Operational semantics for IMP}
\item Specification problem with denotational semantics and its solution
\item Assurance of termination and accessibility predicate
\item Solution in simultaneous induction-recursion
\item Disentangle simultaneous induction-recursion for Coq
\item Conclusion
\end{itemize}
\end{slide}

%-------------------------------------------------------

\overlays{5}{
\begin{slide}{Example}
\vspace{.4in}
\[
\begin{array}{c}
\fromSlide{1}{\whiledo{b}{c}}\\
\\
\fromSlide{2}{\Downarrow}\\
\\
\\
\mbox{\fromSlide{4}{{\gray if}}\  \fromSlide{3}{{\blue $b = \true$}}\ \ \fromSlide{4}{{\gray then} \ \  \{\ \ {\blue $c$}}\fromSlide{5}{$;\ \  {\blue \whiledo{b}{c}}$ \}}}
\end{array}
\]
\end{slide}
}

%-------------------------------------------------------

\overlays{10}{
\begin{slide}{Operational Semantics}
\footnotesize
\[
\fromSlide{1}{\frac{\fromSlide{2}{\opintb{b}{\sigma}{\true}} \quad  \fromSlide{3}{\opintc{c}{\sigma}{\sigma'}} \quad \fromSlide{4}{\opintc{\whiledo{b}{c}}{\sigma'}{\sigma''}}}
     {\opintc{\whiledo{b}{c}}{\sigma}{\sigma''}}
}
\]
\fromSlide{5}{
\begin{center}
$\Downarrow$
\end{center}
}
\[
\fromSlide{6}{
\begin{array}{l}
\opintc{\cdot}{\cdot}{\cdot}\colon {\blue\com\rightarrow\state\rightarrow\state\rightarrow\prop}\\
\vdots\\
\evalwhiletrue\colon \begin{array}[t]{l}
                     {\gray\forall b\colon\bexp; \forall c\colon\com; \forall \sigma,\sigma',\sigma''\colon\state}\\
  \fromSlide{7}{     \opintb{b}{\sigma}{\true}\rightarrow}
  \fromSlide{8}{     \opintc{c}{\sigma}{\sigma'}} \\
  \fromSlide{9}{     \rightarrow \opintc{\whiledo{b}{c}}{\sigma'}{\sigma''}} \\
  \fromSlide{10}{     \rightarrow \opintc{\whiledo{b}{c}}{\sigma}{\sigma''}}
                     \end{array}\\
\end{array}
}
\]
\end{slide}
}

%-----------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\gray Operational semantics for IMP}
\item {\red Specification problem with denotational semantics and its solution}
\item Assurance of termination and accessibility predicate
\item Solution in simultaneous induction-recursion
\item Disentangle simultaneous induction-recursion for Coq
\item Conclusion
\end{itemize}
\end{slide}

%------------------------------------------------------

\overlays{6}{
\begin{slide}{Denotational Semantics}
\footnotesize
\vspace{.5in}
\[
\begin{array}{l}
\fromSlide{1}{\inter{\cdot}\colon{\blue\com\rightarrow\state\rightarrow\state}}\\
\fromSlide{2}{\vdots}\\
\fromSlide{2}{\inter{\whiledo{b}{c}}_\sigma :=}
  \begin{array}{ll}
  \fromSlide{5}{ 
  \inter{\whiledo{b}{c}}}_{\fromSlide{4}{{\inter{c}_\sigma}}} & \mbox{\fromSlide{4}{{\gray if}} \fromSlide{3}{$\inter{b}_\sigma$} \fromSlide{4}{$ = \true$}}\\
  \end{array}
\end{array}
\]
\vspace*{.2in}
\fromSlide{6}{
\begin{itemize}
\item[] {\bf {\red Note}:} Recursive call is not structurally smaller
\end{itemize}}
\end{slide}
}

%------------------------------------------------------

\overlays{11}{
\begin{slide}{Second Order}
\footnotesize
\fromSlide{6}{\includegraphics[width=.15in]{rico_bullet1.ps} Using second order function}
\[
\begin{array}{l}
\untilSlide{5}{f\colon {\blue\com\rightarrow\state\rightarrow\state}}\\
\fromSlide{7}{\Fo\colon {\green(\com\rightarrow\state\rightarrow\state)}}{\blue\fromSlide{8}{\rightarrow\com}\fromSlide{9}{\rightarrow\state}\fromSlide{10}{\rightarrow\state}}\\
\fromSlide{2}{\vdots}\\
\fromSlide{2}{(\fromSlide{6}{{\red\Fo}\ }f\ (\whiledo{b}{c})\ \sigma) :=}\fromSlide{3}{ \left\{
  \begin{array}{ll}
  \fromSlide{5}{(f\ (\whiledo{b}{c})\ }\fromSlide{4}{(f\ c\ \sigma)}\fromSlide{5}{)} \\ \mbox{\fromSlide{4}{{\gray if}} $\inter{b}_\sigma \fromSlide{4}{= \true}$}\\
  \end{array}\right.}
\end{array}
\]
\fromSlide{11}{
\begin{itemize}
\item Apply $\Fo$ as many times as needed
\[
\Fo^k = \lambda g. \underbrace{(\Fo\ (\Fo\ \cdots\ (\Fo}_{\mbox{$k$ times}}\ g)\ \cdots\ ))
\]
\end{itemize}
}
\end{slide}
}

%------------------------------------------------------

\overlays{3}{
\begin{slide}{Equivalence}
\footnotesize
\[
\begin{array}{l}
\fromSlide{1}{{\gray\forall \sigma\colon\state.\forall a\colon\aexp.\forall n\colon\nat.} \ \ \ \ \ \ \opint{a}{\sigma}{n}\  {\red \Leftrightarrow}\  \inter{a}_\sigma = n.}\\
\\
\fromSlide{2}{{\gray\forall \sigma\colon\state.\forall b\colon\bexp.\forall t\colon\bool.}  \ \ \ \ \ \ \;\;\opint{b}{\sigma}{t}\  {\red \Leftrightarrow}\  \inter{b}_\sigma = t.}\\\\
\fromSlide{3}{{\gray\forall c\colon\com.\forall \sigma_1,\sigma_2\colon\state.}}\\
\fromSlide{3}{\opint{c}{\sigma_1}{\sigma_2}\  {\red\Rightarrow}} \\
\fromSlide{3}{\exists k{\gray\colon\nat}.\ \ \forall g{\gray\colon\com\rightarrow\state\rightarrow\state}.
(\Fo^k\ g\ c\ \sigma_1)=\sigma_2}
\end{array}
\]
\end{slide}
}

%------------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\gray Operational semantics for IMP}
\item {\gray Specification problem with denotational semantics and its solution}
\item {\red Assurance of termination and accessibility predicate}
\item Solution in simultaneous induction-recursion
\item Disentangle simultaneous induction-recursion for Coq
\item Conclusion
\end{itemize}
\end{slide}

%------------------------------------------------------

\overlays{2}{
\begin{slide}{Characterizing terminating programs}
\[
\fromSlide{1}{
\begin{array}{l}
D\colon {\blue \com\rightarrow\state\rightarrow\prop}\\
(D\ c\ \sigma) := \begin{array}[t]{l}
                  \exists k{\gray\colon\nat}.\ \ \ \
                  \forall g_1,g_2{\gray\colon\com\rightarrow\state\rightarrow\state}.\\                  (\Fo^k\ g_1\ c\ \sigma) = (\Fo^k\ g_2\ c\ \sigma).
                  \end{array}
\\
\\
\\
\\
\end{array}}
\]

\fromSlide{2}{
Let's try:
\[
c:=\scolon{\whiledo{\true}{\skp}}{{\red \exception}}.
\]}
\end{slide}
}

%------------------------------------------------------

\overlays{8}{
\begin{slide}{Accessibility predicate}
\footnotesize
\vspace{.2in}
\fromSlide{1}{\includegraphics[width=.15in]{rico_bullet1.ps} For simple recursion:
\[
\left\{
\begin{array}{l}
f(e) := \cdots f(e_1) \cdots f(e_2) \cdots\\
\fromSlide{3}{\Acc (e_1) \rightarrow} \fromSlide{4}{\Acc (e_2) \rightarrow} \fromSlide{2}{\Acc (e)}
\end{array}\right.}
\]
\fromSlide{5}{\includegraphics[width=.15in]{rico_bullet1.ps} What will happen for nested recursion?}
\[
\fromSlide{5}{\left\{ 
\begin{array}{l}
f(e) := \cdots f(f(e')) \cdots\\
\fromSlide{7}{\Acc(e') \rightarrow} \fromSlide{8}{{\red \Acc(f(e'))} \rightarrow} \fromSlide{6}{\Acc(e)}
\end{array}\right.}
\]
\end{slide}
}

%------------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\gray Operational semantics for IMP}
\item {\gray Specification problem with denotational semantics and its solution}
\item {\gray Assurance of termination and accessibility predicate}
\item {\red Solution in simultaneous induction-recursion}
\item Disentangle simultaneous induction-recursion for Coq
\item Conclusion
\end{itemize}
\end{slide}

%------------------------------------------------------

\begin{slide}{Example}
\vspace{.4in}
\[
\begin{array}{c}
\whiledo{b}{c}\\
\\
\Downarrow\\
\\
\\
\mbox{{\gray if}\  \fbox{\blue $b = \true$}\ \ {\gray then} \ \  \{\ \ \fbox{\fbox{{\blue $c$}}\ ;\ \  {\blue $\whiledo{b}{c}$}} \}}
\end{array}
\]
\end{slide}


%-------------------------------------------------------

\overlays{8}{
\begin{slide}{Simultaneous induction-recursion}
\scriptsize
\[
\begin{array}{l}
\fromSlide{1}{\comAcc\colon {\blue\com \rightarrow \state \rightarrow \prop}\\}
\fromSlide{7}{\evalcom{\cdot}{}{}\colon {\blue(c\colon \com; \sigma\colon \state) (\comAcc\ c\ \sigma)\rightarrow \state}}\\
\\
\fromSlide{2}{\vdots}
\\
\fromSlide{2}{
\accWhiletrue\colon}
  \begin{array}[t]{l}
\fromSlide{2}{  {\gray \forall b\colon\bexp; \ \forall c\colon\com; \ \forall \sigma\colon\state.}}\fromSlide{3}{ \ \ \inter{b}=\true}\\
\fromSlide{4}{  \rightarrow ({\red h}\colon (\comAcc\ c\ \sigma))}
\fromSlide{5}{  ({\red h'}\colon (\comAcc\ (\whiledo{b}{c})\ \evalcom{c}{\sigma}{h}))}\\
\fromSlide{6}{  \rightarrow (\comAcc (\whiledo{b}{c})\ \sigma)}
  \end{array}
\\
\fromSlide{8}{ \vdots}
\\
\fromSlide{8}{
\evalcom{\whiledo{b}{c}}{\sigma}
        {(\accWhiletrue\ b\ c\ \sigma\ p\ h\ h')}
  := \evalcom{\whiledo{b}{c}}{\evalcom{c}{\sigma}{h}}{h'}
}
\\
\fromSlide{8}{\vdots}
\\
\end{array}
\]
\end{slide}
}

%------------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\gray Operational semantics for IMP}
\item {\gray Specification problem with denotational semantics and its solution}
\item {\gray Assurance of termination and accessibility predicate}
\item {\gray Solution in simultaneous induction-recursion}
\item {\red Disentangle simultaneous induction-recursion for Coq}
\item Conclusion
\end{itemize}
\end{slide}

%------------------------------------------------------

\overlays{6}{
\begin{slide}{Extending $\ldots$}
\scriptsize
\[
\begin{array}{l}
\fromSlide{1}{\comAcc\colon} \\
\fromSlide{1}{{\blue \com \rightarrow \state \rightarrow \nat \rightarrow
              (\com\rightarrow\state\rightarrow\state) \rightarrow \prop}}\\
\fromSlide{2}{\vdots}\\
\fromSlide{2}{
\accWhiletrue\colon}
  \begin{array}[t]{l}
\fromSlide{2}{{\gray \forall b\colon\bexp; \ \forall c\colon\com; \ \forall \sigma\colon\state;}}\\
\fromSlide{2}{{\gray \forall k\colon \nat; \ \forall f\colon\com\rightarrow\state\rightarrow\state.}}\\
\fromSlide{3}{\opint{b}{\sigma}{\true}}\\
\fromSlide{4}{\rightarrow (\comAcc\ c\ \sigma\ k\ f)} \\
\fromSlide{5}{\rightarrow (\comAcc\ (\whiledo{b}{c})\ {\red (F^k_f\ c\ \sigma)})}\\
\fromSlide{6}{\rightarrow (\comAcc (\whiledo{b}{c})\ \sigma\ (k+1)\ f)}
  \end{array}\\
\fromSlide{2}{\vdots}
\end{array}
\]
\end{slide}
}

%------------------------------------------------------

\overlays{2}{
\begin{slide}{Using Accessibility Predicate}
\scriptsize
\vspace{.2in}
\fromSlide{1}{\includegraphics[width=.15in]{rico_bullet1.ps}Defining domain }
\[
\begin{array}{l}
\fromSlide{1}{\comdom \colon {\blue \com\rightarrow\state\rightarrow\set}}\\
\fromSlide{1}{(\comdom\ c\ \sigma) = \Sigma k{\gray\colon \nat}.\forall f{\gray \colon
\com\rightarrow\state\rightarrow\state}. (\comAcc\ c\ \sigma\ k\ f)}\\
\\
\end{array}
\]

\fromSlide{2}{\includegraphics[width=.15in]{rico_bullet1.ps}Defining execution function }
\[
\begin{array}{l}
\fromSlide{2}{\evalcom{\cdot}{}{} \colon
  \begin{array}[t]{l}
  (c\colon \ldots;\ \ \ \sigma\colon \ldots;
   \ \ \ f\colon \ldots)\
  (\comdom\ c\ \sigma)\rightarrow \state
  \end{array}}\\
\\
\end{array}
\]
\end{slide}
}

%------------------------------------------------------

\begin{slide}{Finally $\ldots$}
\scriptsize
\[
\begin{array}{l}
\\
\\
{\gray \forall c\colon\com.\forall \sigma,\sigma'\colon\state.}\\
\opint{c}{\sigma}{\sigma'} {\red \Leftrightarrow}\\
\exists H{\gray\colon (\comdom\ c\ \sigma)}.\ \
\forall f{\gray\colon\com\rightarrow\state\rightarrow\state}.\ \ \ \  \evalcom{c}{\sigma,f}{H} = \sigma'.
\end{array}
\]
\end{slide}

%------------------------------------------------------

\begin{slide}{Where we are?}
\footnotesize
\vspace{.2in}
\begin{itemize}
\item {\gray A small imperative language - IMP}
\item {\gray Operational semantics for IMP}
\item {\gray Specification problem with denotational semantics and its solution.}
\item {\gray Assurance of termination and accessibility predicate}
\item {\gray Solution in simultaneous induction-recursion}
\item {\gray Disentangle simultaneous induction-recursion for Coq}
\item {\red Conclusion}
\end{itemize}
\end{slide}

%------------------------------------------------------

\overlays{2}{
\begin{slide}{Conclusion}
\footnotesize
\begin{itemize}
\item[]
\item[]
\item \fromSlide{1}{Developed operational and denotational semantics inside type theory(Coq)}
\item[]
\item \fromSlide{2}{Have a soundness and completeness theorem stating operational and denotational semantics agree}
\end{itemize}
\vspace*{1in}
\end{slide}
}

%------------------------------------------------------

\begin{slide}{}
\vspace{1in}
\begin{center}
Merci!
\end{center}
\end{slide}

%------------------------------------------------------

\end{document}

