Stefan pushed to branch unification at Stefan / Typer
Commits: 663b82a1 by Stefan Monnier at 2016-11-08T17:38:34-05:00 * doc/rapport: Remove (split into the report/vincent branch)
- - - - -
10 changed files:
- − doc/rapport/Makefile - − doc/rapport/cc.tex - − doc/rapport/gest-proj.tex - − doc/rapport/glossary.tex - − doc/rapport/infer.tex - − doc/rapport/main.tex - − doc/rapport/pres-univ.tex - − doc/rapport/remerciements.tex - − doc/rapport/title.sty - − doc/rapport/typer.tex
Changes:
===================================== doc/rapport/Makefile deleted ===================================== --- a/doc/rapport/Makefile +++ /dev/null @@ -1,46 +0,0 @@ - -TARGET := report -DVI := pdflatex -BIB := biber -IDX := makeindex -PDF := ps2pdf -PS := dvips -GLOS := makeglossaries -OBJDIR := out - -LATEXFLAGS := -output-directory $(OBJDIR) -interaction=batchmode - -MAIN := main - -all: dvi copy - -dvi: - @mkdir -p $(OBJDIR) - @echo -e "First compilation" - @$(DVI) $(LATEXFLAGS) $(MAIN).tex - @echo -e "Generating index" - @$(IDX) $(OBJDIR)/$(MAIN).idx - @echo -e "Generating bibliography" - @$(BIB) --output-directory $(OBJDIR) $(MAIN) - @echo -e "Generating glossary" - @$(GLOS) -q -d $(OBJDIR) $(MAIN) - @echo -e "Second compilation" - @$(DVI) $(LATEXFLAGS) $(MAIN).tex - @$(DVI) $(LATEXFLAGS) $(MAIN).tex - -ps: dvi - @$(PS) $(MAIN).dvi - -pdf: ps - @$(PS) $(MAIN).ps - -copy: - @cp $(OBJDIR)/$(MAIN).pdf $(TARGET).pdf - -latexmk: - latexmk --output-directory=./$(OBJDIR) -pvc main.tex - cp main.pdf $(TARGET).pdf - -clean: - @echo -e "Cleaning" - @rm -f $(MAIN).{ps,pdf,log,aux,out,dvi,bbl,blg}
===================================== doc/rapport/cc.tex deleted ===================================== --- a/doc/rapport/cc.tex +++ /dev/null @@ -1,17 +0,0 @@ -\chapter{Conclusion} - -Ce stage m'a permis de découvrir une partie de l'informatique que nous n'avons pas vu en cours: -les mécanismes d'inférence de type et l'interprétation de langage fonctionnel. -Il m'a permis de découvrir le $\lambda{}-calcul$, modèle de calcul utilisé pour l'implémentation des compilateurs -de langage fonctionnel. - -L'inférence de type d'un langage de programmation fonctionnel est fortement liée à la théorie du $\lambda{}-calcul$. -En effet, le type d'unification utilisé dans ces langages est un sous-ensemble d'un problème indécidable. -Par conséquent, lors de la création du langage, il faut faire attention à ne pas sortir de ce sous-ensemble. -De plus, la représentation interne utilisée par le compilateur influe beaucoup sur les algorithmes -utilisés par l'inférence de type. - -Le langage \typer{} et son compilateur étant en cours de développement, les -seul programmes écrit dans ce langage servent à tester le compilateur. -La création de programmes de moyenne ou grande taille permettra d'évaluer les avantages et les inconvénients de langages -sécurisé de la flexibilité pour cette sécurité.
===================================== doc/rapport/gest-proj.tex deleted ===================================== --- a/doc/rapport/gest-proj.tex +++ /dev/null @@ -1,66 +0,0 @@ -\chapter{Gestion de Projet} - -\section{Planning} - -\structpar{planning} -Le stage a été découpé en quatre parties. - -\begin{figure}[!h] - \centering - \caption{Planning du stage} -\label{tab:plan} - \begin{tabular}{|l | l | l |} - \toprule - partie & durée & résumé \ - \midrule - première partie & une semaine & familiarisation avec le code et les outils utilisés\ - \midrule - deuxième partie & quatre semaines & Implémentation de l'unification de premier ordre\ - \midrule - troisième partie & trois semaines & Implémentation de l'inversion des substitutions d'index de \textit{de Bruijn}\ - \midrule - quatrième partie & quatre semaines & Intégration de l'unification dans l'inférence de type et résolution des bugs\ - \bottomrule - \end{tabular} -\end{figure} - -Les deux dernières semaines ont été laissées libres pour être utilisées pour résoudre les problèmes survenus lors de -l'implémentation des différentes parties ou au cas où une des parties du planning durerait plus longtemps que prévu. -\structpar{gantt} -\begin{figure}[!h] - \centering - \includegraphics[width=1\linewidth]{./plan-1.png} - \caption{Première partie du diagramme de Gantt} -\label{fig:gant1} -\end{figure} -\begin{figure}[!h] - \centering - \includegraphics[width=1\linewidth]{./plan-2.png} - \caption{Deuxième partie du diagramme de Gantt} -\label{fig:gant2} -\end{figure} -\structpar{rythmes des contacts} -Le rythme des contacts avec mon tuteur de stage était d'une fois par semaine. Ces contacts servaient à -faire un compte rendu de mon avancement durant cette semaine. -De plus, je pouvais contacter mon tuteur en cas de besoin, pour résoudre un problème théorique par exemple. - -\section{Cahier des charges} - -\structpar{cahier des charges} -Le but de ce stage était d'implémenter une première version d'inférence de type pour le compilateur -du langage \typer{}. - -\structpar{définition de l'inférence de type} -L'inférence de type est une technique permettant à un compilateur de déduire le type d'une expression. -L'inférence de type de \typer{} doit permettre au système de type de fournir un typage fort. - -L'inférence de type de \typer{} est proche de l'inférence de type de \textit{Hindley-Milner} et doit permettre -d'écrire du code sans aucune annotation de type. - -\structpar{contraintes techniques} -Le code du compilateur de \typer{} est hébergé sur un dépôt gitlab. -L'implémentation de l'inférence de type devait être codée dans le même langage que le compilateur: \texttt{ocaml}. -Les outils de compilation et débogage étaient ceux fournis avec le compilateur \texttt{ocaml}: \texttt{ocamlbuild} et \texttt{make} -pour la compilation et \texttt{ocamldebug} pour le débogage. - -Chaque partie du code devait être testée grâce à un framework de test créé pour le compilateur.
===================================== doc/rapport/glossary.tex deleted ===================================== --- a/doc/rapport/glossary.tex +++ /dev/null @@ -1,16 +0,0 @@ - -\newglossaryentry{lexp}% -{% - name=\lexpgl,% - description={Lambda-Expression}% -} -\newglossaryentry{sexp}% -{% - name=\sexpgl,% - description={S-Expression}% -} -\newglossaryentry{pexp}% -{% - name=\pexpgl,% - description={Proto Lambda-Expression}% -}
===================================== doc/rapport/infer.tex deleted ===================================== --- a/doc/rapport/infer.tex +++ /dev/null @@ -1,189 +0,0 @@ -\chapter{L'inférence de type} - \section{Parser} - - \structpar{Fonctionnement général du parser} - L'interprétation du code se fait de cette façon: - - \begin{center} - code typer $\xrightarrow[]{prelexer}$ code \say{prélexé} $\xrightarrow[]{lexer}$ \sexp{} $\xrightarrow[]{}$ \pexp{} $\xrightarrow[]{}$ \lexp.\ - \end{center} - - \structpar{Les \sexp{}} - Les \texttt{S-Expressions} (\textit{Symbolic expressions}) sont une structure de données en forme d'arbre. - Cette structure de données a été inventée et utilisée pour la première fois par le langage \textit{Lisp}. - Les \sexp{} permettent de représenter un arbre de syntaxe abstrait c'est pourquoi elles ont été utilisées - comme représentation interne du compilateur. - - \structpar{Les \pexp{}} - Les \texttt{Proto Lambda-Expression} sont une représentation à mi-chemin entre les \sexp{} et les \lexp{}. - Elles sont utilisées uniquement pour faciliter la transformation des \sexp{} en \lexp{}. - - \structpar{Les \lexp{}} - Les \lexp{}~\ref{fig:ocmllxp} sont des expressions représentant les \textit{Lambda-Expressions} du $\lambda{}-calcul$. - Elles servent de représentation intermédiaire du code \typer{}. - Les différentes opérations, comme la vérification de type, se font sur les \lexp{}. - - \structpar{Détails} - Lors de l'interprétation du code, il est tout d'abord \say{prélexé}. - Durant cette phase, les commentaires sont supprimés, les litéraux (nombres et chaines de caractères) - sont séparés du code et le code est séparé selon les parenthèses. - - Ensuite, le code \say{prélexé} passe par le lexer qui va transformer le code en \sexp{}. - Les \sexp{} sont ensuite transformées en \pexp{}. - Enfin, les \pexp{} sont transformés en \lexp{}. Durant cette phase, les informations de type vont être rajoutées aux \lexp{}. - - \structpar{L'inférence de type et l'unification} - L'inférence de type se fait sur les \lexp{}. En effet ce sont les seules expressions - à avoir une information sur leur type. - - \section{Unification} - \structpar{Définition} - L'unification est un moyen permettant de déterminer si - % De plus, "déterminer si" donne l'impression que le ŕesultat est - % seulement booléen, alors que l'instantiation des métavariables est - % aussi très important. - deux expressions peuvent être rendues équivalentes. - Dans le cas de l'inférence de type pour le compilateur \typer{}, - l'unification se fait sur les \lexp{}. - Deux \lexp{} sont unifiables si elles sont équivalentes. Si les expressions $S$ et $T$ - sont unifiables alors on peut écrire (en \typer{}) $S = T$. - - Dans le cas du compilateur \typer{}, l'unification est utilisée pour inférer les types - et réduire le nombre d'annotation de type. - - On note $e_1 \unif e_2$ l'unification de $e_1$ et $e_2$. - - \structpar{Exemple} - Par exemple: - \begin{itemize} - \item $3 + 3 \unif 2 * 3$ puisque ces deux opérations sont équivalentes. - \item $(X, (5, 6)) \unif (A, X)$, avec $X = A$ et $X = (5, 6)$. - \item $1 + 2 \nunif "3"$ puisque les deux expressions n'ont pas le même type. - \end{itemize} - - \subsection{Unification de premier ordre} - - \structpar{Définition des méta-variable} - Une méta-variable sert de variable fictive et sera remplacée dès qu'on peut - associer cette méta-variable à une expression. - - Dans le reste du rapport, les méta-variables seront notées en majuscule. - % Par exemple: - % TODO : mettre un exemple - - \structpar{L'unification des \lexp} - L'unification de premier ordre permet de déterminer si deux \lexp{} sont équivalentes, dans les cas simples. - Cependant, toutes les informations nécessaires ne sont pas toujours disponibles lors de l'unification. - L'algorithme d'unification renvoie une liste de contraintes et une liste d'associations entre une méta-variable et une \lexp{} quelconque. - Le couple formé par ces deux listes est appelé le \textit{contexte d'unification}~\ref{fig:ctxunif}. - - \structpar{Cas Évident} - Si deux \lexp{} sont équivalentes, elles sont unifiables. Par exemple, deux nombres égaux seront transformés en deux \lexp{} équivalentes. - Ces deux \lexp{} seront unifiables. - Dans ce cas, l'algorithme d'unification renvoie le même \textit{contexte d'unification} qui lui a été donné en paramètre. - - Respectivement, deux \lexp{} peuvent être facilement identifiées comme non unifiables. Par exemple, les \lexp{} générées par deux nombres différents - ne seront pas unifiables. - Dans ce cas, l'algorithme d'unification renvoie une erreur. En effet, l'unification de deux \lexp{} non unifiables correspond, - dans l'inférence de type, à une erreur de typage. - - \structpar{Cas qui renvoie une contrainte} - Certains cas ne permettent pas de donner une réponse sur le résultat de l'unification. En effet, les informations disponibles - ne sont pas suffisantes. C'est notamment le cas avec les variables et les fonctions. - Dans ce cas, l'algorithme d'unification peut renvoyer une contrainte indiquant que les deux \lexp{} doivent être unifiables. - Plus tard dans l'exécution, cette contrainte sera validée, si le code est correct, ou invalidée, s'il y a une erreur de type. - La liste des contraintes du \textit{contexte d'unification} est représentée sous la forme d'une liste de couples. - Chaque couple représentant de \lexp{} qui doivent être unifiables pour que le typage soit correct. - L'algorithme d'unification renvoie, dans le cas où il doit générer une contrainte, le \textit{contexte d'unification} passé en paramètre - en rajoutant dans la liste des contraintes le couple formé par les deux \lexp{} passées en paramètre. - - \structpar{Méta-variables} - Lorsque l'algorithme d'unification rencontre une méta-variable, il l'associe à l'autre \lexp{} passée en paramètre. - Si la méta-variable est déjà associée à une \lexp{}, alors l'algorithme essaiera d'unifier la \lexp{} associée à la méta-variable - et la \lexp{} passée en paramètre. - Si la méta-variable n'est pas associée à une \lexp{}, l'algorithme renvoie le \textit{contexte d'unification} auquel est rajoutée une - association entre la \lexp{} et la méta-variable. Sinon, l'algorithme renvoie le résultat de l'unification de la \lexp{} passée en paramètre - avec la \lexp{} associée à la méta-variable. - - \structpar{Résultat de l'algorithme} - Le résultat de l'alogrithme permet donc de déterminer quel cas il à rencontré: - \begin{itemize} - \item Si la liste d'association est la même en entrée et en sortie alors les deux \lexp{} passées en paramètre sont unifiables. - \item Si l'unification ne renvoie rien les \lexp{} passée en paramètre ne sont pas unifiables. - \item Si la liste des contraintes renvoyé par l'unification contient une contrainte de plus alors l'unification ne possédait pas assez d'information pour renvoyer un resultat. - \item Si la liste d'association renvoyé par l'unification contient une association de plus alors une des deux \lexp{} passée en paramètre était une méta-variable. - \end{itemize} - - \structpar{Ce qu'il manque} - L'unification de premier ordre ne tient pas en compte des ajouts et suppressions de variables. C'est pourquoi cette forme d'unification ne suffit - pas pour l'inférence de type requise par \typer{}. - - Par exemple, si on essaie d'unifier - \begin{equation} - \verb!x + let x = 5 in x * y! \label{eq:first} - \end{equation} - avec - \begin{equation} - \verb!A + let x = B in A * C! \label{eq:sec} - \end{equation} - l'unification renverra un résultat correct avec $A = x$. Cependant, le premier $x$ et le second $x$ de la première expression (~\autoref{eq:first}~) - ne correspondent pas à la même variable. L'unification devrait donc renvoyer une erreur. - - \subsection{Unification des \hop{}} - \structpar{\hop{}} - L'unification de premier ordre ne suffit pas pour l'inférence de type requise par \typer{}. - En effet, l'unification de premier ordre ne tient pas compte des modifications des index de \textit{de Bruijn}. - L'unification de \typer{} utilise un sous-ensemble de l'unification des \hop{} - L'unification des \hop{} est un sous-ensemble décidable de l'unification d'ordre supérieur. - - L'équation - \begin{equation} - F\ x\ y \unif x + y - \end{equation} - est un \hop{}. La solution de l'unification est $F = \lambda\ a\ b\ \rightarrow a + b$. - \begin{equation} - F\ x\ 1 \unif x + 1 - \end{equation} - n'est pas un \hop{}. Il y a plusieurs solutions non équivalentes: $F = \lambda\ x\ y \rightarrow x + y$ et $F = \lambda\ x\ y \rightarrow x + 1$ - - \structpar{Les index de \textit{de Bruijn}} - Les index de \textit{de Bruijn} sont une notation inventée par Nicolaas Govert de Bruijn qui sert à représenter les - termes du $\lambda{}-calcul$. Cette notation utilise des index comme identificateur de variables (dans le code). L'index le plus grand - correspond à la première variable instanciée (et toujours définie). - - Les index de \textit{de Bruijn} facilitent la comparaison de variable par rapport à l'utilisation de nom de variable comme identifiant. - En effet, deux variables peuvent avoir le même nom de variable tout en étant différentes. Avec l'utilisation des index de \textit{de Bruijn}, - ces deux variables auront des index différents puisqu'elles sont différentes. - Cependant, le décalage des index lié à l'ajout et la suppression de variables peut causer des erreurs lors de la comparaison d'une même - variable dans des contextes différents. - - Par exemple l'expression: - \begin{equation} - \lambda\ x \rightarrow (x, \lambda\ y \rightarrow x + y) - \end{equation} - sera encodé par: - \begin{equation} - \lambda \rightarrow (#0, \lambda \rightarrow #1 + #0) - \end{equation} - - \structpar{La substitution des index de \textit{de Bruijn}} - Pour remédier au problème de l'ajout et de la suppression de variables avec les index de \textit{de Bruijn}, on associe au contexte des - variables une substitution. Cette substitution, une fois appliquée à un index, l'augmente ou le réduit. - Ceci permet de modifier les index en fonction du contexte et pouvoir comparer des variables dans différents contextes. - - \structpar{L'unification avec les index de \textit{de Bruijn}} - Pour prendre en compte les différences de contexte lors de l'unification, il faut intégrer - les substitutions d'index de \textit{de Bruijn} dans l'unification. - Pour cela, on associe à une meta-variable l'inverse de la substitution en cours. De cette - façon, les \texttt{Metavar} (représentation des méta-variables dans le compilateur) ne représentent plus - des méta-variables mais l'application d'une substitution à une méta-variable. - Cette modification permet de prendre en compte le contexte dans lequel la méta-variable a été créée - et ainsi de pouvoir appliquer les substitutions lors de l'unification de variables dans des contextes différents. - - Par exemple si on considère $A[\sigma]$ avec $A$ une méta-variable et $\sigma$ la substitution appliquée à $A$. - $A$ est une méta-variable, sa valeur n'est pas connue. Il faut donc garder la substitution suspendue. - Pour résoudre $A[\sigma] \unif e$, avec $e$ une expression quelconque, il faut donc résoudre $A = e[\sigma^{-1}]$. - - $\sigma^{-1}$ est la substitution inverse de $\sigma$ tel que $\sigma^{-1} \circ \sigma = id$ et $e[\sigma^{-1} \circ \sigma] = e[id] = e$. - - % TODO : mettre un exemple concrèt ?
===================================== doc/rapport/main.tex deleted ===================================== --- a/doc/rapport/main.tex +++ /dev/null @@ -1,176 +0,0 @@ -\documentclass[a4paper, 15pt]{report} - -\usepackage[utf8]{inputenc} -\usepackage[T1]{fontenc} -\usepackage[pdftex]{graphicx} -\usepackage[backend=biber]{biblatex} -\usepackage[left=2cm,right=2cm,top=2.5cm,bottom=2cm]{geometry} -\usepackage{amssymb} -\usepackage{amsmath} -\usepackage{hyperref} -\usepackage{multirow} -\usepackage{booktabs} -\usepackage{makeidx} -\usepackage{filecontents} -\usepackage{listings} -\usepackage{color} -\usepackage{verbatim} -\usepackage[toc]{glossaries} -\usepackage{newunicodechar} % for \newunicodechar -\usepackage{title} -\usepackage{siunitx} -\usepackage[french]{babel} -\usepackage[left=\flqq, right=\frqq, leftsub=\flqq, rightsub=\frqq]{dirtytalk} - -\begin{filecontents*}{\jobname.bib} -@misc{ - udemnum, - title = { http://recteur.umontreal.ca/documents-institutionnels/faits-et-chiffres/%7D -} -@misc{ - wikinum, - title = { http://fin.umontreal.ca/direction-finances/etats-financiers/documents/ef%5C_... } -} -\end{filecontents*} - -\addto\captionsfrench{\renewcommand{\chaptername}{Partie}} - -\addbibresource{\jobname.bib} - -\lstset{language=caml, - basicstyle=\ttfamily, - keywordstyle=\color{blue}\ttfamily, - stringstyle=\color{red}\ttfamily, - commentstyle=\color{green}\ttfamily, - morecomment=[l][\color{magenta}]{#} -} - -\AtBeginDocument{\renewcommand{\ref}[1]{(cf~\autoref{#1})}} - -\setcounter{secnumdepth}{3} - -\newcommand{\udem}{Université de Montréal} -\newcommand{\typer}{\textit{Typer}} -\newcommand{\sexpgl}{\texttt{S-exp}} -\newcommand{\lexpgl}{\texttt{L-exp}} -\newcommand{\pexpgl}{\texttt{P-exp}} - -\newunicodechar{≡}{\ensuremath{\equiv}} -\newunicodechar{α}{\ensuremath{\alpha}} - -\DeclareMathOperator{\unif}{\mathbin{=?}} -\DeclareMathOperator{\nunif}{\mathbin{\neq?}} - -\title{Stage de quatrième année} -\subtitle{Développement d'inférence de type pour le langage Typer} -\author{BONNEVALLE Vincent} -\tuteurPoly{Guillaume Raschia} -\tuteurEntr{Stéfan Monnier} -\scolaryear{2015 -- 2016} -\thisyear{4} -\logo{% -\includegraphics[scale=0.5]{./img/udem.png}}{% -\includegraphics[scale=0.5]{./img/univ-nantes.png}}{% -\includegraphics[scale=0.5]{./img/polytech.png}% -} - -\makeindex -\makeglossaries -\input{./glossary.tex} - -\newcommand{\sexp}{\gls{sexp}\index{sexp@S-Expression}} -\newcommand{\lexp}{\gls{lexp}\index{lexp@Lambda-Expression}} -\newcommand{\pexp}{\gls{pexp}\index{pexp@P-Expression}} -\newcommand{\hop}{\textit{High Order Pattern}} - -\newboolean{release} -\newcommand{\release}[1]{\setboolean{release}{#1}} -\newcommand{\structpar}[1]{% - \ifthenelse{\boolean{release}}% - {\paragraph{}}% - {\paragraph{#1}}% -} - -\newboolean{outline} -\newcommand{\outline}[1]{\setboolean{outline}{#1}} - -\release{true} -\outline{false} -%% \par est équivalent à une ligne blanche - -\begin{document} - \maketitle - \tableofcontents - \clearpage - - \input{remerciements.tex} - \input{pres-univ.tex} - \input{gest-proj.tex} - \input{typer.tex} - \input{infer.tex} - \input{cc.tex} - \clearpage - - \appendix - \thispagestyle{empty} - \pagenumbering{roman} - - % TODO : remplir les parties dessous - % TODO : rajouter les citations ... - % \listoftables - \listoffigures - - \clearpage - \chapter*{Annexes} - \begin{figure}[h] - \centering - \verbatiminput{test2.typer} - \caption{Exemple de code typer} - \label{code:typer} - \end{figure} - \clearpage - \begin{figure}[h] - \centering - \begin{lstlisting}[language=caml] -type ltype = lexp - and lexp = - | Imm of sexp - | SortLevel of sort_level - | Sort of U.location * sort - | Builtin of vdef * ltype - | Var of vref - | Susp of lexp * subst - | Let of U.location * (vdef * lexp * ltype) list * lexp - | Arrow of arg_kind * vdef option * ltype * U.location * lexp - | Lambda of arg_kind * vdef * ltype * lexp - | Call of lexp * (arg_kind * lexp) lis - | Inductive of U.location * label - * ((arg_kind * vdef * ltype) list) - * ((arg_kind * vdef option * ltype) list) SMap.t - | Cons of vref * symbol - | Case of U.location * lexp - * ltype - * ltype - * (U.location * (arg_kind * vdef option) list * lexp) SMap.t - * lexp option - | Metavar of int * subst * vdef - \end{lstlisting} - \caption{Définition des \lexp{}} - \label{fig:ocmllxp} - \end{figure} - \begin{figure}[h] - \centering - \begin{lstlisting}[language=caml] -type substitution = lexp VMap.t (* VMap.t est une table associative *) -type constraints = (lexp * lexp) list -type unification_ctx = (substitution * constraints) - \end{lstlisting} - \caption{Contexte d'unification} - \label{fig:ctxunif} - \end{figure} - \clearpage - - \printindex - % \printglossaries - \printbibliography -\end{document}
===================================== doc/rapport/pres-univ.tex deleted ===================================== --- a/doc/rapport/pres-univ.tex +++ /dev/null @@ -1,51 +0,0 @@ -\chapter{Présentation de l'\udem{}} - - \section{L'université} - - \structpar{Chiffres} - L'\udem{} est une université située à Montréal au Canada. - Elle a été créée en 1878. - Une partie de l'université, dont le département informatique est située sur le Mont Royal. - L'école vétérinaire de l'université est à Sainte-Hyacinte, hors de Montréal. - Le reste de la faculté se situe sur le campus de Laval à Montréal. - Enfin, un nouveau campus est en train de se développer à Outremont et pourrait à terme remplacer celui du Mont Royal. - - Elle est classée première université du Québec\cite{udemnum} et deuxième université du Canada\cite{udemnum}, que ce soit en nombre - d'étudiants ou pour la recherche. - - \structpar{Chiffres} - Cette université accueille près de \num{67 000} étudiants et \num{2 700} chercheurs dans 16 facultés et écoles\cite{udemnum}. - Elle dispose d'un budget de \num{1,05} milliard de dollars canadiens\cite{wikinum} (en 2014). - - L'\udem{} propose des programmes dans différents domaines d'études comme le droit, les sciences, la littérature \dots - \begin{figure}[!h] - \centering - \includegraphics[width=0.8\linewidth]{./img/DSCN0360.JPG} - \caption{\udem{}} -\label{fig:udem} - \end{figure} - \clearpage - - \section{Le département informatique} - - \structpar{Cursus possibles} - Le département informatique propose plusieurs cursus allant du développement web à la compilation. - - \structpar{LTP} - Le laboratoire dans lequel j'ai fait mon stage est le Laboratoire de Traitement Parallèle. - Il est composé de deux professeurs: Stefan Monnier et Marc Feeley. - - Initialement, ce laboratoire était dédié à des travaux sur le parallélisme. - Cependant, actuellement, le sujet de recherche des professeurs de ce laboratoire est la compilation. - \begin{figure}[!h] - \centering - \includegraphics[width=0.8\linewidth]{./img/DSCN0410.JPG} - \caption{Laboratoire de Traitement Parallèle} -\label{fig:ltp} - \end{figure} - - \structpar{Stefan Monnier} - Mon tuteur de stage était Stefan Monnier. Actuellement, ses sujets de recherche sont les langages de programmation fortement typés et les - langages sécurisés ainsi que les répercussions de ces langages sur les compilateurs, les \textit{runtimes system} et les systèmes d'exploitations. - Ces recherches l'ont amené à créer le langage \typer{} qui sert de preuve de concept pour un langage sécurisé et qui fournit des outils - pour la création de preuves de logiciels.
===================================== doc/rapport/remerciements.tex deleted ===================================== --- a/doc/rapport/remerciements.tex +++ /dev/null @@ -1,8 +0,0 @@ -\chapter*{Remerciements} -Je tiens à remercier particulièrement mon tuteur monsieur Stefan Monnier de m'avoir accueilli dans son laboratoire -et de m'avoir permi de travailler sur un sujet que je n'aurai pas eu l'occasion d'étudier autrement. -Je le remercie aussi pour l'aide qu'il m'a apportée pendant ces treize semaines. - -Grâce à ce stage j'ai aussi eu la possibilité de découvrir Montréal. - -Je remercie aussi toutes les personnes que j'ai cotoyées dans ce laboratoire pour leur accueil chaleureux.
===================================== doc/rapport/title.sty deleted ===================================== --- a/doc/rapport/title.sty +++ /dev/null @@ -1,50 +0,0 @@ - -\ProvidesPackage{title} - -\RequirePackage{graphicx} - -\newcommand*{\subtitle}[1]{\gdef@subtitle{#1}% -} -\newcommand*{@subtitle}{} - -\newcommand*{\tuteurPoly}[1]{\gdef@tuteurPoly{#1}} -\newcommand*{\tuteurEntr}[1]{\gdef@tuteurEntr{#1}} - -\newcommand*{\logo}[3]{\gdef@logo{#1\hfill#2\hfill#3}% -} -\newcommand*{@logo}{} - -\newcommand*{\scolaryear}[1]{\gdef@scolaryear{#1}} - -\newcommand*{\thisyear}[1]{\gdef@thisyear{#1}} - -\renewcommand*{\maketitle}{% -\begin{titlepage} -\parindent 0pt -INFO @thisyear \hfill Tuteur de stage : @tuteurEntr\ -Année @scolaryear \hfill Enseignant responsable : @tuteurPoly\ - -\vfill - -\begin{flushleft} - \usefont{OT1}{ptm}{m}{n} - \Large @title\ :\ - \Huge @subtitle -\end{flushleft} - -\par -\hrule height 4pt -\par - -\begin{flushright} - \usefont{OT1}{phv}{m}{n} - \Large @author - \par -\end{flushright} - -\vfill - -@logo -\end{titlepage} -} -\endinput
===================================== doc/rapport/typer.tex deleted ===================================== --- a/doc/rapport/typer.tex +++ /dev/null @@ -1,38 +0,0 @@ -\chapter{Le langage \typer{}} - - \section{Présentation du langage} - \structpar{Description} - \typer{} est un langage de programmation fonctionnel pur. Il est total, typé statiquement et avec des types dépendants. - Les macros de \typer{} permettent de faire de la méta-programmation et d'étendre le langage - - Dans la suite du rapport, \say{\typer{}} fera référence au langage \typer{} et \say{le compilateur \typer{}} fera référence au compilateur - interprétant le langage \typer{} - - \structpar{Inspirations} - \typer{} est inspiré de \textit{Lisp}, \textit{Coq} et \textit{ML}. - Il est conceptuellement proche de \textit{Coq} (langage pur, total, typé statiquement et avec des types dépendants). Cependant, le but de \typer{} - est d'écrire des programmes et non des preuves. - Le système de macros de \typer{} est inspiré de \textit{Lisp}, il permet d'étendre facilement le langage - en manipulant le code comme des données. De plus, comme pour \textit{Lisp}, la syntaxe de \typer{} est stratifiée. - La syntaxe du code est proche de la syntaxe de \textit{ML}. L'inférence de type de \typer{} est un sur-ensemble de l'inférence de type - \textit{Hindley-Milner} - \structpar{Spécificités} - Les macros de \typer{} devraient, à terme, pouvoir être utilisées pour construire des preuves de programmes. - - \section{Motivations} - \typer{} est un langage dont le but est de fournir des moyens d'écrire du code sûr. - En effet, les outils qu'il devrait fournir, à terme, facilitent l'écriture de code correct. - Par exemple, le compilateur de \typer{} peut vérifier qu'il n'y aura pas de récursion infinie. - De plus, les macros du langage devrait permettre, à terme, d'écrire des preuves de code. - - \section{État de l'implémentation} - \structpar{Avant} - Au début de mon stage, les bases du langage étaient implémentées: - la définition et l'appel de lambda, la création de type ainsi que la création de variables étaient supportées par le compilateur. - L'inférence de type n'étant pas implémentée, le compilateur requérait le typage explicite des variables et des paramètres de fonction. - Le compilateur fournissait peu de fonctions et opérations. - - \structpar{Après} - `A la fin du stage, une version basique de l'inférence de type était en cours d'intégration: il restait quelques bogues à résoudre avant que - cette version soit fonctionnelle. En effet, l'intégration de l'unification au système de typage a requis certaines modifications dans - ce système. Ces modifications ont mis en évidence des erreurs qui n'ont pas pu être résolues à temps.
View it on GitLab: https://gitlab.com/monnier/typer/commit/663b82a1e297ea509b9199169d9f797d434d...
Afficher les réponses par date