Commit ebca6e8a authored by Guillaume G's avatar Guillaume G

Merge branch 'master' of https://git.lsv.fr/genestier/mi-parcours

parents 05d28e18 50204db3
......@@ -444,7 +444,7 @@ dont je vais chercher le premier dans quelques mois.
\bibliographystyle{plain}
\bibliography{../Bureau/Utiles/Zotero,more}
\bibliography{../Bureau/Utiles/biblio,more}
\newpage
\section{Curriculum du doctorat}
......@@ -545,7 +545,7 @@ Un s\'ejour d'un mois \`a Chalmers University, G\"oteborg, Su\`ede est pr\'evu d
\item \`A venir : 11th International School on Rewriting, 1-6 juillet 2019, Paris, France, 36h
\item 2018 EUTypes Summer School on
Types for Programming and Verification,
8-12 ao\^ut 2018, Ohrid, Macedoine, 25h
8-12 ao\^ut 2018, Ohrid, Macédoine, 25h
\end{itemize}
\noindent{\large Transverses (46h effectu\'ees) :}
......
......@@ -65,12 +65,12 @@
\begin{frame}
\frametitle{Sommaire}
\tableofcontents[currentsection,hideothersubsections]
\end{frame}
\end{frame}
}
\begin{frame}[fragile]\frametitle{\emph{Dedukti}}
\emph{Dedukti} est un vérificateur de typage pour le $\lambda\Pi$-calcul modulo réécriture.
\begin{block}{Exemple de type dépendant}
\begin{lstlisting}
def F : Nat -> TYPE
......@@ -166,10 +166,10 @@ def sum : (n: Nat) -> F n
\section{Critères de terminaison}
\subsection{Paires de dépendances}
\subsection{Paires de dépendance}
\begin{frame}\frametitle{Paires de dépendances}
\begin{defi}[Paires de dépendances]
\begin{frame}\frametitle{Paires de dépendance}
\begin{defi}[Paires de dépendance]
Une règle $f\,\bar l \to r$ engendre les \emph{paires de dépendance} $f\,\bar l > g\,\bar m$ si :
\begin{itemize}
\item $g$ est (partiellement) défini par réécriture,
......@@ -179,8 +179,8 @@ Une règle $f\,\bar l \to r$ engendre les \emph{paires de dépendance} $f\,\bar
\begin{thm}[Arts et Giesl]
Au premier ordre :
$\to_{\mathcal{R}}$ termine ssi il n'existe pas $f\,\bar t>g\,\bar u\to_{arg}^*g\,\bar u'>\dots$
$\to_{\mathcal{R}}$ termine ssi il n'existe pas $f\,\bar t>g\,\bar u\to_{arg}^*g\,\bar u'>\dots$
\end{thm}
\end{frame}
......@@ -191,7 +191,7 @@ def plus : Nat -> Nat -> Nat.
[n] plus 0 n --> n.
[m,n] plus (S m) n --> S (plus m n). $\color{red}(1)$
[m,n] plus m (S n) --> S (plus m n). $\color{red}(2)$
def append: (p: Nat) -> List p ->
(q: Nat) -> List q -> List (plus p q).
[q,m] append _ nil q m --> m.
......@@ -216,7 +216,7 @@ def plus : Nat -> Nat -> Nat.
[n] plus 0 n --> n.
[m,n] plus (S m) n --> S (plus m n). $\color{red}(1)$
[m,n] plus m (S n) --> S (plus m n). $\color{red}(2)$
def append: (p: Nat) -> List p ->
(q: Nat) -> List q -> List (plus p q).
[q,m] append _ nil q m --> m.
......@@ -242,13 +242,13 @@ def append: (p: Nat) -> List p ->
\begin{frame}{Size-Change Termination}
\begin{block}{Principe}
Exclure les cycles apparaissant dans le graphe d'appels.
Suivre la taille des arguments au cours des appels de fonction.
\end{block}
Prenons un ordre {\color{red} bien fondé} sur les termes.
Prenons un ordre {\color{red} bien fondé} sur les termes.
\vspace{1em}
Supposons qu'il y ait une chaîne infinie de paires de dépendance.
\vspace{1em}
......@@ -262,7 +262,7 @@ def append: (p: Nat) -> List p ->
\begin{frame}[fragile]\frametitle{Size-Change Termination : Exemple}
Variation de la taille des arguments :\vspace{1em}
\begin{tabular}{|l|c|}
\hline
......@@ -332,7 +332,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\item Lambda abstraction,
\item Application partielle et application de variables,
\begin{lstlisting}
[f,x,l] map f (Cons x l) --> Cons (f x) (map f l)
[f,x,l] map f (cons x l) --> cons (f x) (map f l)
\end{lstlisting}
\item Réécriture au niveau type.
......@@ -408,11 +408,11 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\end{frame}
\begin{frame}\frametitle{Les paires de dépendance reviennent}
\begin{defi}[Plain Function Passing]
$f\,\bar l\to r$ est \emph{PFP} si toutes les variables apparaissant dans $r$ qui sont de type fonctionnel sont égales à l'un des $l_i$.
\end{defi}
\begin{lem}
Tout $f$ est dans l'interprétation de $\Theta_f$ si:
\begin{itemize}
......@@ -463,12 +463,12 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\draw[>=latex,->,color=darkgreen] (ast) to (type_cstr);
\draw[>=latex,->,color=red] (ast) to[bend left] (dk_sign);
\draw[>=latex,->,color=red] (symb_ord) to (dk_pruned);
\draw[>=latex,->,double] (dk_sign) to (sr);
\draw[>=latex,->,double] (dk_pruned) to (pos);
\draw[>=latex,->,double] (call_gr) to (sct);
\draw[double] (type_gr) to[out=0] (7,0.5);
\draw[double] (type_cstr) to[out=0,in=-140] (7,0.5);
\draw[>=latex,->,double] (7,0.5) to (well-struct);
\draw[>=latex,->,ultra thick] (dk_sign) to (sr);
\draw[>=latex,->,ultra thick] (dk_pruned) to (pos);
\draw[>=latex,->,ultra thick] (call_gr) to (sct);
\draw[ultra thick] (type_gr) to[out=0] (7,0.5);
\draw[ultra thick] (type_cstr) to[out=0,in=-140] (7,0.5);
\draw[>=latex,->,ultra thick] (7,0.5) to (well-struct);
\node[draw] (leg) at (-2.4,-2.4) {\begin{tabular}{ll}
{\color{blue}$\to$}&Parseur\\
{\color{red}$\to$}&Traduction vers Dedukti\\
......@@ -500,7 +500,7 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
Exemple : Ordinaux de Brouwer (\lstinline{lim : (Nat -> Ord) -> Ord.})
\begin{itemize}
\item Présent dans beaucoup d'encodages de logiques,
\item Première version écrite.
\item Première version écrite, d\'ej\`a impl\'ement\'ee.
\end{itemize}
\end{block}
......@@ -533,15 +533,15 @@ $\color{red}{(3)}$ append _ (cons x p l) q m
\begin{block}{Cet été}
Séjour à G\"oteborg pour traduire Agda dans Dedukti et réciproquement.
\end{block}
\begin{block}{fin 2019}
\begin{block}{Fin 2019}
\'Ecrire un article sur l'extension aux types positifs.
\end{block}
\begin{block}{Arrive très vite}
\begin{itemize}
\item \'Ecrire une thèse,
\item R\'edaction,
\item Soutenance en septembre 2020.
\end{itemize}
\end{block}
\end{frame}
\end{document}
\ No newline at end of file
\end{document}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment