diff --git a/Slides/SlidesFSCD.tex b/Slides/SlidesFSCD.tex index 660e2d6bb4852418e254b94621044aea42730cff..b73e1d24bc2b2efcd22a9360c4358edc783e21f9 100644 --- a/Slides/SlidesFSCD.tex +++ b/Slides/SlidesFSCD.tex @@ -294,7 +294,7 @@ def sum : (n: Nat) -> F n \newcommand{\ens}[1]{\left\{#1\right\}} \newcommand{\enscond}[2]{\ens{\left.\vphantom{#2}#1\right|#2}} -\section{Termination criterion} +\section{Termination Criterion} \begin{frame}\frametitle{Main Goal} @@ -303,7 +303,7 @@ def sum : (n: Nat) -> F n \LARGE If $\Gamma\vdash t:T$, then $t\in\mathrm{SN}(\to_{\beta\mathcal{R}})$. \end{frame} -\subsection{Logical relation} +\subsection{Logical Relations} \begin{frame}\frametitle{Logical Relations} \begin{block}{Goal} @@ -394,7 +394,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m $\color{red}{>}$ p + q \end{frame} -\begin{frame}[fragile]\frametitle{Call-graph: Example} +\begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. set infix "+" := plus. @@ -423,15 +423,15 @@ def append: (p: Nat) -> List p -> \end{center} \end{frame} -\subsection{Well-structuring} +\subsection{Well-Structuring} -\begin{frame}\frametitle{Well-structuring} +\begin{frame}\frametitle{Well-Structuring} \begin{block}{} $\succeq$ quasi-order on the signature compatible with rewriting and typing. \end{block} -\begin{definition}[Well-structured system]\label{def-well-struct} +\begin{definition}[Well-Structured System]\label{def-well-struct} $\mathcal{R}$ is \emph{well-structured} if for all rule $(\Delta,f\,\bar l\to r)$, with $\Theta_f=\Pi(\bar x:\bar T).U$, we have $\Delta\vdash_{\!\!\preceq f} r:U[\bar x\to \bar l]$. @@ -475,7 +475,7 @@ def append: (p: Nat) -> List p -> \subsection{Size-Change Termination} -\begin{frame}[fragile]\frametitle{Call-graph: Example} +\begin{frame}[fragile]\frametitle{Call-Graph: Example} \begin{lstlisting}[mathescape=true] def plus : Nat -> Nat -> Nat. set infix "+" := plus.