main.tex 8.23 KB
Newer Older
Kim Nguyễn's avatar
Kim Nguyễn committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
\documentclass[DIV=11,10pt]{scrartcl}

\usepackage[cm]{fullpage}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
% \usepackage[utf8]{eurosym}
\usepackage[french]{babel}

\usepackage{hyperref}

\usepackage[T1]{fontenc}
% \usepackage{lmodern}
\usepackage{microtype}

\usepackage{xcolor}
\usepackage{paralist}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
17
\usepackage{alltt}
Kim Nguyễn's avatar
Kim Nguyễn committed
18
19
20
21
22
23
24
25
26
27
28
29

\usepackage{amsmath,amssymb}
\usepackage{cleveref}

% \usepackage{fourier}
\usepackage{tgadventor}

\usepackage[backend=biber,style=numeric,firstinits=true,maxbibnames=99,url=false%
            % url=false,doi=false,isbn=false
            ]{biblatex}

\usepackage{xspace}
Kim Nguyễn's avatar
Kim Nguyễn committed
30
\newcommand{\code}[1]{\texttt{#1}}
Kim Nguyễn's avatar
Kim Nguyễn committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
% \addtokomafont{disposition}{\rmfamily}
\addtokomafont{descriptionlabel}{\rmfamily}

% Please use \hhnote etc... for comments, feel free to tweak to your
% liking.
\usepackage{fixme}
\fxsetup{theme=color,mode=multiuser}
\FXRegisterAuthor{eg}{aneg}{\color{blue}EG}
\FXRegisterAuthor{gc}{angc}{\color{blue}GC}
\FXRegisterAuthor{hh}{anhh}{\color{blue}HH}
\FXRegisterAuthor{tz}{antz}{\color{blue}TZ}

\title{...}

\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
\author{Giuseppe Castagna, Kim Nguyen}
\date{\today}

\begin{document}
\maketitle
% Après pour parler science, on souhaitait te faire travailler sur une
% théorie et mise unifiée d'un langage de programmation moderne,
% statiquement typé avec le sous-typage sémantique au cœur du système.
% Le constat est que même si la méta-théorie de semsub + X  est écrite
% et marche (où X \in { polymorphisme, gradual, occurrence typing }),
% mettre le tout dans un langage sans que ça casse, avec une
% méta-théorie unique pose de gros challenge, de formalisation et
% d'implémentation (est-ce que ça peut être fait de manière « modulaire
% » ?)

% Certains points sont encore balbutiant : occurence typing (manque
% l'analyse de flot de contrôle), gestion des effets dans un tel langage
% (grosse inconnue), inférence de type, notion de type principale (au
% moins pour un fragment du langage) sont des axes de recherche
% complètement nouveau.

% Pour les aspects de transfert ou d'impact dans l'industrie, il y a une
% application directe de ce travail pour l'inférence de type de code
% Javascript pour pouvoir l'utiliser dans la base de données Oracle. Je
% viens de recevoir un grant d'Oracle pour étudier ces aspects, et ton
% travail poserait les fondements théoriques pour développer de tels
% outils.


% Voilà, on te tient au courant, avec la propal détaillée et les infos
% de comment on se réparti l'encadrement. Essaye d'avoir la date exacte
% de la deadline pour qu'on ne la rate pas :-)


\section{Description du sujet}

Cette thèse s'inscrit dans la thématique des langages de programmation
et en particulier dans celle des langages de programmation
statiquement typés. Dans un tel langage, des règles de typage
permettent de garantir l'absence de certaines classes d'erreurs à
l'exécution.
Un exemple simple de règle de typage est celle qui
demande que l'opérateur de soustraction ne soit \emph{bien typé} que
sur des arguments numériques. Elle permet ainsi de détecter des
Kim Nguyễn's avatar
Kim Nguyễn committed
90
erreurs du programmeur qui essayerais de soustraire un tableau et une
Kim Nguyễn's avatar
Kim Nguyễn committed
91
92
93
94
95
96
chaîne de caractères (code qui n'aurait aucun sens). Les \emph{types}
sont objets associés aux expressions et valeurs du langage décrivant
leur domaine. Par exemple le type \texttt{Int} associé au constantes
\texttt{1}, \texttt{2}, \ldots indique que de telles valeurs sont des
entiers.

Kim Nguyễn's avatar
Kim Nguyễn committed
97
98
99
100
101
102
103
104
105
106
107
108
109
Le contexte de la thèse est plus précisément celui des langages de
programmation muni d'un système de type \emph{ensembliste}. 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
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 ensembliste d'union, d'intersection ou de
complémentaire, traditionnellement absent des langages de
programmation généralistes.

Une première étape dans la théorie et conception des langages de
programmation à types ensembliste a été la définition et
l'implantation du langage CDuce \cite{}.
Kim Nguyễn's avatar
Kim Nguyễn committed
110
111
112
113
114
115
116
117
118
119










Giuseppe Castagna's avatar
Giuseppe Castagna committed
120
121
Le but the cette thèse est d'arriver à définir et étudier un langage de programmation fonctionnel statiquement typé qui combine les characteristiques avancée suivantes:
\begin{enumerate}
Kim Nguyễn's avatar
Kim Nguyễn committed
122

Giuseppe Castagna's avatar
Giuseppe Castagna committed
123
  \item typage d'occurrence
Kim Nguyễn's avatar
Kim Nguyễn committed
124

Giuseppe Castagna's avatar
Giuseppe Castagna committed
125
  \item types ensemeblistes (types union, intersection et négation)
Kim Nguyễn's avatar
Kim Nguyễn committed
126

Giuseppe Castagna's avatar
Giuseppe Castagna committed
127
  \item typage graduel
Kim Nguyễn's avatar
Kim Nguyễn committed
128

Giuseppe Castagna's avatar
Giuseppe Castagna committed
129
  \item polymorphisme paramètrique et inférence de types
Kim Nguyễn's avatar
Kim Nguyễn committed
130

Giuseppe Castagna's avatar
Giuseppe Castagna committed
131
132
133
  \item types recursifs
    
  \item effets et ordre supérieur
Kim Nguyễn's avatar
Kim Nguyễn committed
134

Giuseppe Castagna's avatar
Giuseppe Castagna committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  \item raffinement de types  

\end{enumerate}
Nous allons montrer par des exemples l'intérêt de chaque characteristique:

\paragraph{Typage d'occurrence}
Le typage de occurrence, ou \emph{occurrence typing} est un technique
qui analyse les test effectués par un programme pour pouvoir raffiner
l'analyses de types dans le code à executer en cas de reussite ou
d'échec du test. Un example d'application du typage d'occurrence est donné par le
code suivant JavaScrip
\begin{alltt}
  function foo(x) {
      (typeof(x) === "number")? x++ : x.trim()
  }
\end{alltt}
Dans ce code on teste si l'argument de la fonction \code{x} 


Initialement défini pour Scheme il est de plus en plus développé dans
l'industrie (Hack, Typescript, Flow) car il est indispensable pour
pourvoir analyses the programming patterns typiques de la
programmation en langages dynamiques.




CHALLENGES

Tous ces sujets ont été étudiés separament ainsi que pour certains
leur combinaison. Mais l'integration de toutes ses characteristiques
ensemble pose de nouveaux défis qui demande non seulment des avances
sur chaqun de ses sujets mais ...
Kim Nguyễn's avatar
Kim Nguyễn committed
168
169
170
171




Kim Nguyễn's avatar
Kim Nguyễn committed
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200



\section{Contexte Sociétal, Économique et Industriel}
Un résultat immédiat de cette thèse est la possibilité de typer, au
moins partiellement, des programmes écrits dans des langages
dynamiques tels que JavaScript ou Python. En effet, le typage
d'occurrence et les types ensemblistes permettent d'analyser des
programmes ayant des comportements non-uniformes selon le type de leurs
entrées, ce qui est une caractéristique des langages
dynamiques. L'inférence de type permet de déduire le types de tels
programmes même en l'absence d'annotations de type de la part du
programmeur. Enfin, le typage graduel permet de typer partiellement
des programmes et de circonscrire précisément les parties trop «
dynamiques » n'ayant pas pu être analysées.

Cette analyse statique de langages dynamiques est particulièrement
importante dans le contexte actuel de la science des données. En
effet, les langages de choix des analystes de données sont usuelement
des langages dynamiques (en particulier Python pour la physique, R
pour les statistiques et JavaScript pour la programmation
Web). L'amélioration de tels langages dans ce contexte est l'un des
objectifs de la chaire de recherche « Langages de programmation
Orientés Données » de la fondation Paris-Saclay, portée par K. Nguyen.
Cette chaire, financée par une donnation d'Oracle Labs. Il est prévu
que la chaire prennent entre autre en charge les missions du doctorant
ou de la doctorante retenu pour cette thèse.


Kim Nguyễn's avatar
Kim Nguyễn committed
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
\section{Déroulement de la thèse}
\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
suffisemment 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
raisonnablement efficace (en particulier de l'algorithme de génération
de contraintes pour le typage polymorphe).

\subsection{Deuxième année}
L'objectif, ambitieux, est l'intégration d'un système d'effets au
langage purement fonctionnel défini lors de la première année. La
combinaison entre types ensemblistes, polymorphismes et effets n'a
jusqu'à présent jamais été étudiée. 

Kim Nguyễn's avatar
Kim Nguyễn committed
220
221
222
223
224
225
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: