% !TeX spellcheck = fr_FR
\documentclass[12pt]{beamer}

% Loading packages
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{bbm}
\usepackage{stmaryrd}
\usepackage[main=french,english]{babel}
\usepackage{csquotes}
\usepackage{listings}
\usepackage{lstautogobble}
\usepackage{algorithm2e}
\usepackage{svg}
\usepackage{tikz}
\usepackage{multirow}
\usepackage{multicol}
\usepackage{tcolorbox}
\usepackage{mdframed}
\usepackage{proof}
\usepackage{biblatex}
\usepackage{xparse}
\usepackage{cprotect}
\usepackage{xpatch}
\usepackage{amsfonts}
\usepackage{mathtools}
\usepackage{setspace}
\usepackage{pdfpc}

\usepackage{geometry}
\usepackage{subcaption}

\usepackage{csquotes}
\usepackage[lighttt]{lmodern}
\usetikzlibrary{shapes.geometric,positioning}

% Macros caractères globales
\newcommand{\pgrph}{\P}
\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
\renewcommand{\P}{\mathbb{P}}
\newcommand{\E}{\mathbb{E}}
\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}}
\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
\newcommand{\littleO}{o}
\newcommand{\bigO}{\mathcal{O}}
\newcommand{\longdash}{\:\textrm{---}\:}
\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}
\newcommand\bracket[1]{\!\left[#1\right]}
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}}
\newcommand\spacebar{\;|\;}
\def\nDownarrow{\not\mspace{1mu}\Downarrow}
\let\pprec\preccurlyeq

\DeclareUnicodeCharacter{03BB}{$\lambda$}
\DeclareUnicodeCharacter{03B1}{$\alpha$}
\DeclareUnicodeCharacter{03C0}{$\pi$}

% Création des environnement globaux
\newtheorem{property}{Propriété}

\newcounter{rule}

% Commandes logiques globales
\newcommand{\ifnullthenelse}[3]{
	\ifnum\value{#1}=0
	#2
	\else
	#3
	\fi
}

%%% Commande \newtag permettant de changer le label d'une equation
\makeatletter
\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
\makeatother


% Macros caractères spécifiques au document
\newcommand{\methprec}[1]{\prec\mkern-8mu\left[\fj{#1}\right]}
\DeclareMathOperator{\varnull}{varnull}
\DeclareMathOperator{\nextop}{next}
\DeclareMathOperator{\new}{\text{\textbf{new}}}
\DeclareMathOperator{\CT}{CT}
\DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}}
\newcommand\subclass{\mathrel{<:}}
\newcommand\superclass{\mathrel{:>}}
\newcommand\OKin{\text{\textnormal{\textsc{ OK in }}}}

% Création des environnements spécifiques au document

%%% Blocs colorés pour le code FeatherweightJava
\newtcbox{\fjmaincodebox}{nobeforeafter,tcbox raise base, arc=0pt, outer arc=0pt, boxsep=0pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=0pt,colback=white!85!black}
\newtcbox{\fjind}{nobeforeafter,tcbox raise base, rounded corners=all, boxsep=0pt,left=1pt,right=1pt,top=1pt,bottom=1pt,boxrule=0pt,colback=white!52!orange}
\newenvironment{fjlisting}[1][]
{
	\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!96!black,#1]
		\ttfamily
	}{
	\end{tcolorbox}
}

% Langage Featherweight Java
\makeatletter
\newcommand*\idstyle{%
	\expandafter\id@style\the\lst@token\relax
}
\def\id@style#1#2\relax{%
	\ifcat#1\relax\else
	\ifnum`#1=\lccode`#1%
	\ttfamily
	\fi
	\fi
}
\makeatother
\lstdefinelanguage{FeatherweightJava}{
	keywords = {new, this, true, false},
	basicstyle=\ttfamily,
	identifierstyle=\idstyle,
	literate=%
	{à}{{\`a}}1
	{é}{{\'e}}1
	{è}{{\`e}}1
	{ù}{{\`u}}1
}
\lstset{literate=%
	{à}{{\`a}}1
	{é}{{\'e}}1
	{è}{{\`e}}1
	{ù}{{\`u}}1}

%% Commande 4
\NewDocumentEnvironment{textenv}{b}{\text{\textnormal{#1}}}{}
%\lstMakeShortInline[language=FeatherweightJava]|
\newcommand{\fj}[1]{\begin{textenv}\lstinline[language=FeatherweightJava,mathescape=true]~#1~\end{textenv}}



% Définition des macros pour l'écriture des trucs Featherweight Java
\newcommand\fjattr{\GenericWarning{$\backslash$ fjattr doit être utilisé dans une fjclass}}
\newcounter{fjargcount}
\newcommand{\fjparamattributes}[2][Object]{
	\null\qquad #1 #2;\newline
}
\newcommand{\printcomma}{,}
\newcommand{\fjparamconstparameters}[2][Object]{
	\ifnullthenelse{fjargcount}{}{,$\text{ }$} \text{#1} \;\text{#2}
	\stepcounter{fjargcount}
}
\newcommand{\fjparamconstassign}[2][Object]{
	\null\qquad\qquad \textbf{this}.#2 = #2;\newline
}
\newcommand{\fjmethod}[4]{
	\null\qquad #1 #2(#3)\{\newline
	\null\qquad\qquad \textbf{return} \lstinline[language=FeatherweightJava]{#4};\newline
	\null\qquad\}\newline
}

\newcommand{\fjmain}[1]{
	\noindent\fjmaincodebox{\lstinline[language=Java]{#1}}
}

% Premier argument: Nom de la classe
% Second argument: \fjattr{x}[Object] \fjattr{attr}[A]
% Troisième argument \fjmethod{C}{metname}{Object w, B par}{((D)obj).apply(par)} plusieurs fois
% Argument optionnel: la classe que l'on extend
\newcommand{\fjclass}[4][Object]{%
	\noindent \textbf{class} #2 \textbf{extends} #1 \{\newline
	% Attributs
	\let\fjattr\fjparamattributes
	#3
	% Constructeur
	\let\fjattr\fjparamconstparameters
	\setcounter{fjargcount}{0}
	\null\qquad #2(\ifx&#3&\else $#3$\fi) \{\newline
	\null\qquad\qquad \textbf{super}();\newline
	\let\fjattr\fjparamconstassign%
	#3
	\null\qquad\}\\
	% Méthodes
	#4
	\}
}

\addbibresource{Bilibibio.bib}

\usetheme{Madrid}

\hypersetup{pdfpagemode=FullScreen}
% Transition en fade-in par défaut
\addtobeamertemplate{background canvas}{\transfade[duration=0.4]}{}

\addtobeamertemplate{frametitle}{
	\let\insertframetitle\insertsubsectionhead}{}
\makeatletter
\CheckCommand*\beamer@checkframetitle{\@ifnextchar\bgroup\beamer@inlineframetitle{}}
\renewcommand*\beamer@checkframetitle{\global\let\beamer@frametitle\relax\@ifnextchar\bgroup\beamer@inlineframetitle{}}
\makeatother

\setbeamertemplate{itemizeitem}{\scriptsize$\diamond$}

\author{Samy Avrillon}
\title{Définition d'un préordre sur les programmes Featherweight Java}
\subtitle{Notes sur mon stage au LACL}
\newif\ifplacelogo % create a new conditional
\placelogotrue % set it to true
\logo{\ifplacelogo\includesvg[width=1.5cm]{logoEns}\fi}
\institute{ENS de Lyon}

\begin{document}
	
	\begin{frame}[plain]
		\maketitle
	\end{frame}

	\section*{Sommaire}
	\begin{frame}
		\begin{multicols}{2}
			\tableofcontents[pausesections,hideallsubsections]
		\end{multicols}
	\end{frame}

	\section{Introduction}
	
	\section{Featherweight Java}
		
		\subsection{Sa grammaire}
			\begin{frame}
				
				\begin{center}
					\refstepcounter{rule}
					\begin{tabular}{rll}
						$e$ $:=$\pause & \fj{x} & \qquad \textrm{\textsc{E-Var}} \\
						\pause
						| & \fj{new C($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Cstr}}}{rule:expr:constructor} \\
						\pause
						| & \fj{$e$.f} & \qquad \newtag{\textrm{\textsc{E-Field}}}{rule:expr:field} \\
						\pause
						| & \fj{$e$.m($\overline{e}$)} & \qquad \newtag{\textrm{\textsc{E-Meth}}}{rule:expr:method} \\
						\pause
						| & \fj{(C)$e$} & \qquad \newtag{\textrm{\textsc{E-Cast}}}{rule:expr:cast}
					\end{tabular}
				\end{center}
				\pause
				\[\fj{new Paire((D)new B().get(), new C(new A())).snd.apply()}\]
			\end{frame}
		\subsection{Ses structures}
			\begin{frame}
				\pause
				\textbf{Class table} \only<3>{$+$ \textbf{Expression} = \textbf{Programme}}
				\begin{fjlisting}
					\textbf{class} A \textbf{extends} Object \{...\}\\
					\textbf{class} B \textbf{extends} Object \{...\}\\
					\fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}\\
					\pause
					\fjmain{new Paire(new A(), new B())}
				\end{fjlisting}
				
			\end{frame}
			
		\subsection{Sa réduction}
			
			\begin{frame}
				\pause
				\begin{itemize}[<+->]
					\item $\fj{new C(e1,e2,...,en).field} \rightarrow \fj{ek}$ (\textsc{R-Field})
					\item $\fj{new C(e1,e2,...,en).meth(f1,f2,...,fn)} \rightarrow e_{\fj{C.meth}}\bracket{\fj{new C(e1,e2,...,en)}\middle/ \fj{this},\fj{f1}\middle/\fj{x1},\fj{f2}\middle/\fj{x2},...,\fj{fn}\middle/\fj{xn}}$ (\textsc{R-Invk})
					\item $\fj{(C) expr} \rightarrow \fj{expr}$ (\textsc{R-Cast})
				\end{itemize}
			\end{frame}
			
		\subsection{Son typage}
		
			\begin{frame}
				\pause
				\[\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
				{\fj{x} \in \Gamma}
				\qquad
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
				\]
				\pause
				\vspace{.2ex}
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
				{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
				\]
				\vspace{.2ex}
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
				\]
				\vspace{.2ex}
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
				\qquad
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
				\]
			\end{frame}
		
	\section{Notre problème}
		
		\subsection{Qu'est-ce qu'une équivalence}
			\begin{frame}
				\begin{exampleblock}{Sens}
					\pause
					\begin{itemize}[<+->]
						\item Deux programmes «font la même chose»
						\item Assez stricte
						\item Assez large
					\end{itemize}
				\end{exampleblock}
				\pause
				\begin{exampleblock}{Utilisations}
					\pause
					\begin{itemize}[<+->]
						\item Utiliser un autre algorithme (complexités)
						\item Utiliser une version plus sécurisée
						\item Effectuer une optimisation
					\end{itemize}
				\end{exampleblock}
			\end{frame}
		\subsection{La méthode classique}
			\begin{frame}
				\begin{center}
					Contexte : $C$
					\vspace{2ex}\pause
					
					Contextualisation : $C\bracket{P}$
					\vspace{2ex}\pause
					
					Préordre : $P \prec Q \iff \forall C\quad C\bracket{P} \implies C\bracket{Q}$
					\vspace{2ex}\pause
					
					Équivalence : $P \equiv Q \iff P \prec Q \land Q \prec P$
				\end{center}
			\end{frame}
		
	\section{Idée d'une nouvelle structure}
		
		\subsection{Comparer uniquement les CT}
		\begin{frame}
			\begin{center}
				\pause
				\begin{multicols}{2}
					\null\vfill
					\begin{fjlisting}[width=.49\textwidth]
						\textbf{class} XXX \textbf{extends} XXX \{\}\\
						\vdots\\
						\fjmain{expression}
					\end{fjlisting}
					\vfill\null
					\columnbreak
					\pause
					\begin{fjlisting}[width=.49\textwidth]
						\textbf{class} XXX \textbf{extends} XXX \{\\
						\}\\
						\vdots\\
						\textbf{class} Main \{\\
							\fjmethod{Object}{main}{}{expr}
						\}
					\end{fjlisting}
				\end{multicols}
			\end{center}
			\pause
			\[\fj{new Main().main()}\rightarrow \fj{expr}\]
		\end{frame}
		\subsection{Idée d'une structure}
		\begin{frame}
			\begin{itemize}[<+->]
				\item Besoin de restreindre les contextes
				\item Empêcher au test d'accéder à tout
				\item Utiliser un mécanisme déjà là
				\item Inspiration: \eng{header file} en C
			\end{itemize}
		\end{frame}
		
		\subsection{Exemple et théorème}
			\begin{frame}
				\begin{fjlisting}
					Number \{\}\\\null
					\pause
					
					Int \{\}\\
					Int : Int suivant(Int)\\
					Int : Int add(Int,Int)\\
					Int <: Number
				\end{fjlisting}
			\end{frame}
			\begin{frame}
				\begin{fjlisting}
					Frac(Int numerateur, Int denominateur)\\
					Frac : Frac inverted()\\
					Frac : Int floor()\\
					Frac <: Number\\\null
					\pause
					
					RichInt \{Int value\}\\
					RichInt : Int getInt()\\
					RichInt <: Int
				\end{fjlisting}
			\end{frame}
			\begin{frame}
				\begin{exampleblock}{Relations à créer}
					\pause
					\begin{itemize}
						\item Opérateur d'implémentation ($\triangleright$)
						\pause
						\item Typage avec la TI ($\Vdash$)
						\pause
						\item Validation d'une CT dans une TI
					\end{itemize}
				\end{exampleblock}
				\pause
				\begin{theorem}
					\pause
					\begin{itemize}
						\item $\mathcal{A} \triangleright \mathfrak{T}$
						\item $\mathcal{B} \OKin \mathfrak{T}$
						\item $\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}$
					\end{itemize}
					
					\[\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}\quad\text{et}\quad\fj{C} \subclass \fj{D}\]
				\end{theorem}
			\end{frame}
		
	\section{Formalisation des \eng{test interfaces}}
		
		\subsection{Leur grammaire}
			\begin{frame}
				\pause
				\begin{tcolorbox}[left=5pt,right=2pt,top=5pt,bottom=5pt,boxrule=1pt,rounded corners=all,colback=white!92!blue]
					\begin{center}
						\refstepcounter{rule}
						\begin{tabular}{rll}
							TR := & C : C m($\overline{\fj{C}}$) & \qquad \textrm{\textsc{TIG-Meth}} \\
							| & C \{$\overline{\fj{C}}$ $\overline{\fj{f}}$\} & \qquad \textrm{\textsc{TIG-Attr}} \\
							| & C ($\overline{\fj{C}}$ $\overline{\fj{?}\fj{f}}$) & \qquad \textrm{\textsc{TIG-Cstr}} \\
							| & C <: C & \qquad \textrm{\textsc{TIG-Cast}}
						\end{tabular}
					\end{center}
				\end{tcolorbox}
			\end{frame}
		
		\subsection{L'opérateur d'implémentation}
		
			\begin{frame}
				\[
					\infer
					{\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]}
					{
						\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \fj{$\overline{\texttt{E}}$} \rightarrow \fj{H}
						\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
						\quad \fj{H}\subclass_\mathcal{A}\fj{G}
					}
					\qquad
					\infer
					{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
					{\fj{C} \subclass_\mathcal{A} \fj{D}}
				\]
				\vspace{2ex}
				\[
					\infer
					{\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}
					{
						\overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)
						\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
					}\qquad
					\infer
					{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
					{\begin{array}{l}
							\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\
							\overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\
							\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad 
							\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
						\end{array}
					}
				\]
				
			\end{frame}
		
		\subsection{Nouvelles applications de \eng{lookup}}
			\placelogofalse
			\begin{frame}
				\ttfamily
				\vspace{-3ex}
				\pause
				\begin{center}
					\[
					\onslide<2->{\infer
					{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
					{\left[\fj{C($\overline{\texttt{D}}\;\overline{\texttt{?f}}$)}\right] \in \mathfrak{T}}}
					\qquad
					\onslide<3->{
					\infer
					{\operatorname{fields}(\fj{C}) = \underbrace{\overline{\fj{D}}\;\overline{\fj{f}}}_{\text{\textrm{pour \fj{f} défini}}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
					{\left[\fj{ C ( $\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}}
					}
					\]
					\[
					\onslide<2->{
					\infer
					{\operatorname{construct}(\fj{C}) = \overline{\fj{D}}}
					{\fj{class C\{C($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}}
					}
					\quad
					\onslide<3->{
					\infer
					{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
					{\left[\fj{ C \{ $\overline{\texttt{D}}\;\overline{\texttt{f}}$\}}\right] \in \mathfrak{T}}
					}
					\]
					\vspace{.2ex}
					\onslide<3->{
					\[
					\infer
					{\operatorname{fields}(\fj{C}) = \overline{\fj{D}}\;\overline{\fj{f}} + \bigcup_{C \subclass E}\operatorname{fields}(\fj{E})}
					{\fj{class C \{$\overline{\texttt{D}}\;\overline{\texttt{f}}$; ...\}} \in \mathcal{B}}
					\qquad
					\infer
					{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
					{\left[\fj{ C : E m( $\overline{\texttt{D}}$)}\right] \in \mathfrak{T}}
					\]
					\vspace{.2ex}
					\[
					\infer
					{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
					{\fj{class C \{...; E m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}} \in \mathcal{B}}
					\qquad
					\infer
					{\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}}\rightarrow\fj{E}}
					{\operatorname{mtype}(\fj{m},\fj{C'}) = \overline{\fj{D}}\rightarrow\fj{E}\quad \fj{C} \subclass \fj{C'}}
					\]
					}
				\end{center}
			\end{frame}
			
		\subsection{Nouveau typage}
			\begin{frame}
				\vspace{-2ex}
				\pause
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
				{\fj{x} \in \Gamma}
				\qquad
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
				{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
				\]
				\pause
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
				\]
				\vspace{.3ex}
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
				\]
				\vspace{.3ex}
				\[
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
				\qquad
				\infer
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
				\]
			\end{frame}
			\placelogotrue
		\subsection{Théorème de cohérence}
			\begin{frame}
				\pause
				\begin{theorem}
					\label{thm:tiTyp}
					Soit une \eng{test interface} $\mathfrak{T}$, une \eng{class table} $\mathcal{A}$, un couple $(\mathcal{B},e)$ \eng{class table} $\times$ expression fermée appelée \enquote{test}, et un environnement de typage $\Gamma$ vérifiant
					\begin{itemize}
						\item $\mathcal{A} \triangleright \mathfrak{T}$
						\item $\mathcal{B} \OKin \mathfrak{T}$
						\item $\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}$
					\end{itemize}
					
					Alors il existe \fj{C} tel que $\mathcal{A} \oplus \mathcal{B},\Gamma \vdash e : \fj{C}$ et $\fj{C} \subclass \fj{D}$.
				\end{theorem}
			\end{frame}
		
		\subsection{Définition du préordre}
			 \begin{frame}
			 	\pause
			 	\begin{definition}
			 		Soit une \eng{test interface} $\mathfrak{T}$.
			 		
			 		Soient deux \eng{class tables} $\mathcal{A}$ et $\mathcal{B}$ qui implémentent toutes deux $\mathfrak{T}$
			 		
			 		Alors
			 		\[\mathcal{A} \prec_\mathfrak{T} \mathcal{A'} \ssi \forall (\mathcal{B},e) \left|\begin{array}{l}
			 			\mathcal{B} \OKin \mathfrak{T}\\
			 			\mathfrak{T},\mathcal{B} \Vdash e : \fj{D}\\
			 			\mathcal{A}\oplus\mathcal{B} \Downarrow v
			 		\end{array}\right. \implies \mathcal{A'}\oplus\mathcal{B}\Downarrow v\]
			 	\end{definition}
			 \end{frame}
		
	\section{Les valeurs infinies}
		
		\subsection{Qu'est-ce qu'un context lemma}
			
			\begin{frame}
				\pause
				\[(\mathcal{A},e)\prec(\mathcal{B},f) \implies (\mathcal{A},h\bracket{e})\prec(\mathcal{A},h\bracket{f})\]
			\end{frame}
			
		\subsection{Pourquoi est-il faux ici}
			\placelogofalse
			\begin{frame}
				\begin{fjlisting}
					public Static \{\\
						\fjmethod{IList}{intList}{Int i}{new IList(i, intList(i+1))}
						\fjmethod{IList}{zeroList}{}{new IList(0, zeroList())}
					\}
				\end{fjlisting}
				\vspace{-3ex}
				\begin{gather*}
				e_i = \fj{intList(0)} \rightarrow^*\\ \fj{new IList(0,new IList(1,new IList(2,intList(3))))}\\
				e_0 = \fj{zeroList()} \rightarrow^*\\ \fj{new IList(0,new IList(0,new IList(0,zeroList())))}
				\end{gather*}
			\end{frame}
			\placelogotrue
			\begin{frame}
				\[
				\begin{array}{rcl}
					h\bracket{e_i} &=& \fj{intList(0).next.obj}\\
					&\rightarrow& \fj{new IList(0, intList(0+1)).next.obj}\\
					&\rightarrow& \fj{intList(0+1).obj}\\
					&\rightarrow& \fj{new IList(0+1, intList(0+1+1)).obj}\\
					&\rightarrow& \fj{0+1}\\
					&\rightarrow^{\!*}& \fj{1}\\
					
					h\bracket{e_0} &=& \fj{zeroList().next.obj}\\
					&\rightarrow& \fj{new IList(0, zeroList()).next.obj}\\
					&\rightarrow& \fj{zeroList().obj}\\
					&\rightarrow& \fj{new IList(0, zeroList()).obj}\\
					&\rightarrow& \fj{0}
				\end{array}
				\]
			\end{frame}
		\subsection{Idée de valeurs infinies}
		
		\subsection{Explication de la formalisation}
			\begin{frame}
				\begin{center}
					Comment capturer ces \enquote{valeurs infinies} ?
					
					\vspace{1ex}
					\pause
					Valeurs à variable: $\hbar$
					\[\fj{new C(x,new S(new S(y,new G()),z))}\]
					\pause
					\[\boxed{e\rightarrow^* v \implies f\rightarrow^* v}\Rrightarrow \boxed{\forall \hbar \forall \alpha \; \left(e \rightarrow_\mathcal{A}^* \hbar\bracket{\alpha} \implies \exists \beta\quad f \rightarrow_\mathcal{B}^* \hbar\bracket{\beta}\right)}\]
					\pause
					\[e \rightarrow^* \fj{new C(new D(...))} \implies f \rightarrow^* \fj{new C(new D(...))}\]
					\begin{gather*}
						\fj{new IList(0,new IList(1,...))}\\
						\neq\\
						\fj{new IList(0,new IList(0,...))}
					\end{gather*}
				\end{center}
			\end{frame}
		
		\subsection{Redéfinition des préordres}
			\begin{frame}
				\[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\]
			\end{frame}
		\subsection{Propriétés}
			\begin{frame}
				\pause
				\begin{property}
					\[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\]
				\end{property}
				\pause
				\begin{property}
					\[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\]
				\end{property}
				\pause
				\begin{property}[Context Lemma]
					\begin{gather*}
						\forall \mathcal{A} \quad\forall e,f \quad\forall (h,\mathcal{B})\\
						(e,\mathcal{A})\pprec(f,\mathcal{B}) \implies (h[e],\mathcal{A} \oplus \mathcal{B})\pprec(h[f],\mathcal{A}\oplus\mathcal{B})
					\end{gather*}
				\end{property}
			\end{frame}
	
	\section{Conclusion}
		\subsection{Conclusion}
		\begin{frame}
			\begin{exampleblock}{Résumé}
				\begin{itemize}[<+->]
					\item On a créé un préordre
					\item Assez puissant (sémantique)
					\item Assez tolérant
					\item Context Lemma
					\item Concepts réutilisables
				\end{itemize}
			\end{exampleblock}
			\begin{exampleblock}{Futur}
				\begin{itemize}[<+->]
					\item Formalisation dans un assistant de preuve
					\item Comparer uniquement certains types de retour
					\item Théorèmes pour simplifier l'équivalence
					\item Obtenir des retours
				\end{itemize}
			\end{exampleblock}
		\end{frame}
	
	\begin{frame}
		\Huge\[\mathfrak{FIN}\]
	\end{frame}
\end{document}