Commit 307cd361 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

typos

parent 2179a668
......@@ -47,7 +47,7 @@
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\unk}{\texttt{?}}
\title{Intégration d'outils de programmation avancés dans un lagage avec types ensemblistes}
\title{Intégration d'outils de programmation avancés dans un langage avec types ensemblistes}
\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
\author{Encadrement: Giuseppe Castagna, Kim Nguyen
......@@ -107,7 +107,7 @@ entiers.
Le contexte de la thèse est plus précisément celui des langages de
programmation munis d'un système de types \emph{ensemblistes}. Dans un
tel système, les types ne sont pas simplement des objets syntaxiques
utilisé pour l'analyse (le typage) mais des ensembles de valeurs (au
utilisés pour l'analyse (le typage) mais des ensembles de valeurs (au
sens mathématique). Cette définition \emph{sémantique} des types comme
des ensembles induit une algèbre de types très riche, comprenant par
exemple les opérateurs ensemblistes d'union, d'intersection ou de
......@@ -143,7 +143,7 @@ caractéristiques de programmation avancée suivantes:
Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\paragraph{Typage d'occurrences:}
Le typage de occurrences, ou \emph{occurrence typing}, est une technique
Le typage d'occurrences, ou \emph{occurrence typing}, est une technique
qui utilise les tests effectués par un programme afin de pouvoir raffiner
l'analyse de types dans le code à exécuter en prenant en compte la réussite ou
l'échec du test. Un exemple d'application du typage d'occurrences est donné par le
......@@ -158,10 +158,10 @@ Dans ce code on teste si l'argument de la fonction
\code{number}; si oui on renvoie le successeur de l'argument et si non
on envoie à l'argument le message \code{trim()}. Puisque \code{trim} est une
méthode définie seulement pour les valeurs de type \code{string}
(il s'agit d'une méthode du standard ECMAScript 5 qui élimines les espaces
(il s'agit d'une méthode du standard ECMAScript 5 qui élimine les espaces
au début et à la fin d'une chaîne de caractères) on peut facilement
déduire que l'argument de \code{foo} doit être de type \code{number} ou
\code{string}. C'est à dire il doit avoir le type ``union''
\code{string}. C'est à dire qu'il doit avoir le type ``union''
\code{number|string}. Dans les
systèmes de types standards cette information n'est pas suffisante pour
pouvoir typer la fonction \code{foo} car
......@@ -174,7 +174,7 @@ de manière différente dans chaque branche du test: puisque le programme a test
\code{x} est de type \code{number}, alors nous pouvons supposer que
\code{x} est de type \code{number} dans la branche ``then'' du test, et
qu'il \emph{n'est pas} de type \code{number} dans la branche ``else''
(et de cela et du fait qu'il doit être ou \code{number} ou \code{string} déduire
(et de cela et du fait qu'il doit être ou \code{number} ou \code{string}, déduire
que \code{x} est de type \code{string} dans cette dernière branche).
......@@ -243,7 +243,7 @@ typé moderne pour pouvoir programmer de manière générique et modulaire. Cett
fonctionnalité se retrouve en effet sous le nom de \emph{generics}
dans le langage Java ou encore \emph{template} dans le langage \code{C++} et est l'une des caractéristiques distinctives des langages fonctionnels typés.
Un simple exemple de cette nécessitée peut être obtenu en
Un simple exemple de cette nécessité peut être obtenu en
modifiant légèrement le code de \code{foo} de façon à ce que la branche
``else'' renvoie l'argument inchangé:
\begin{alltt}
......@@ -276,7 +276,7 @@ il renvoie un résultat du même type.
\paragraph{Types récursifs, effets et ordre supérieur:}
Les types récursifs, les
effets et les fonctions d'ordre supérieure sont, à l'instar du
effets et les fonctions d'ordre supérieur sont, à l'instar du
polymorphisme paramétrique, des caractéristiques
importantes dans un langage de programmation moderne. Ici il ne s'agit
pas de trouver des nouvelles fonctionnalités mais d'étudier comment
......@@ -284,29 +284,29 @@ intégrer ces caractéristiques avec celles énoncées ci dessus. En effet,
chacun des traits cités interagit de manière subtile avec le système
de type et la sémantique du langage. Par exemple, la presence d'effets force un
ordre d'évaluation et demande d'imposer certaines restrictions sur le
polymorphisme pour garantir la sûreté du typage. En plus cette
polymorphisme pour garantir la sûreté du typage. De plus, cette
interaction rend les techniques algorithmiques existantes caduques:
par exemple en présence de types ensemblistes les algorithmes
par exemple, en présence de types ensemblistes, les algorithmes
d'unification ne sont plus suffisants pour l'inférence de types
polymorphes.
\paragraph{Raffinement de types:}
nous avons déjà montré deux exemples de raffinent de types: le typage
nous avons déjà montré deux exemples de raffinement de types: le typage
d'occurrences permet de raffiner le type des occurrences d'une
expression de manière différente dans les branches d'un test; une
meilleure inférence des types permettrait de raffiner le type
\code{number|string $\to$ number|string} de \code{foo} dans le type
\code{(number$\to$number)\&(string$\to$string)} qui est bien plus
précis On voudrait ajouter la possibilité de raffiner les types du
langages par le biais de propositions logiques. Par exemple on voudrait
définir le type des nombres impairs comme il suit $\texttt{Odd} = \{
x\in\texttt{Int}~|~x\mod 2 = 1\}$: \texttt{Odd} serait un raffinement du
précis. On voudrait ajouter la possibilité de raffiner les types du
langage par le biais de propositions logiques. Par exemple, on voudrait
définir le type des nombres impairs comme il suit: $\texttt{Odd} = \{
x\in\texttt{Int}~|~x\mod 2 = 1\}$. \texttt{Odd} serait un raffinement du
type \texttt{Int}. Il existe déjà une littérature abondante sur ce
sujet. La spécificité dans cette thèse serait d'utiliser ces types en
combinaison avec les types ensemblistes pour généraliser le typage
d'occurrence: si nous avons un test sur une expression booléenne $e$
et $x$ est une variable libre dans $e$ de type $t$ alors on pourrait
et si $x$ est une variable libre dans $e$ de type $t$, alors on pourrait
raffiner son type par $\{x\in t~|~e\}$ dans la branche ``then'' et
$\{x\in t~|~\neg e\}$ dans la branche ``else''.
......@@ -320,18 +320,18 @@ défis qui demandent non seulement des avancées sur chacun d'eux
mais aussi le développement de nouvelles techniques qui en
permettent la combinaison. L'inférence de types intersection pour les
fonctions nécessitera une analyse fine que sera fournie par le
typage d'occurrence et une analyse de contrôle de flot que on
typage d'occurrence et une analyse de contrôle de flot que l'on
tachera d'intégrer avec cette dernière. Cette analyse pourra aussi
être utilisée pour l'intégration des effets. Pour ces derniers nous
envisageons d'utiliser les travaux sur les effets algébriques en le
envisageons d'utiliser les travaux sur les effets algébriques en les
combinant avec l'expressivité logique des types ensemblistes.
L'inférence de type polymorphe sera basée sur la génération d'ensembles
de contraintes dont la solution utilisera les types récursifs et les
types ensemblistes. Le typage d'occurrence n'est actuellement utilisé
que dans des car très particuliers (des tests des types sur des
variables); il faudra le généraliser à des tests quelconques de types,
que dans des cas très particuliers (des tests de type sur des
variables); il faudra le généraliser à des tests quelconques de type,
en utilisant l'expressivité logique donnée par les types ensemblistes
et pour le combiner avec des types polymorphes. On l'étendra ensuite à
et en le combinant avec des types polymorphes. On l'étendra ensuite à
la présence d'effets. Le typage d'occurrence sera ensuite utilisé pour
optimiser la compilation de systèmes graduels afin de réduire le
nombre de contrôles dynamiques.
......@@ -372,14 +372,14 @@ Conférences en Informatique, LRI, équipe VALS, Université
Paris-Saclay, 50\%).
\subsection{Première année}
L'objectif pour la première année est la définition théorique et implémentation
au sein d'un prototype d'un langage alliant typage d'occurrences,
sous-typage sémantique polymorphisme et inférence de
types. Les points d'attention dans ce premier pan de la recherche sont
en particulier la définition formelle du langage, qui devra être
suffisamment modulaire pour être étendue avec d'autres aspects, un
L'objectif pour la première année est la définition théorique et l'implémentation
d'un prototype de langage alliant typage d'occurrences,
sous-typage sémantique, polymorphisme et inférence de
types. Les points d'attention dans ce premier pan de la recherche sont,
en particulier: la définition formelle du langage (qui devra être
suffisamment modulaire pour être étendue avec d'autres aspects), un
cadre théorique permettant la définition d'heuristiques et leur
expérimentation pour l'inférence de types et un implémentation
expérimentation pour l'inférence de types, et une implémentation
raisonnablement efficace (en particulier de l'algorithme de génération
de contraintes pour le typage polymorphe).
......@@ -392,8 +392,8 @@ jusqu'à présent jamais été étudiée. Elle pose des problèmes théoriques
notion de « réductions parallèles » des sous-termes syntaxiquement
identiques, qui n'est plus possible dès lors que le langage est
impur). Une piste à explorer est l'utilisation d'effets algébriques,
introduits par Plotkin \emph{et al}. \cite{PlotkinP03, PlotkinP13} qui
semble pertinents dans le cadre d'un système de types ensemblistes.
introduits par Plotkin \emph{et al}. \cite{PlotkinP03, PlotkinP13}, et qui
semblent pertinents dans le cadre d'un système de types ensemblistes.
\bibliographystyle{unsrt}
\bibliography{main}
......
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