main.tex 16.9 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

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

% \usepackage{fourier}
\usepackage{tgadventor}


\usepackage{xspace}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
27
\usepackage{bm}
Kim Nguyễn's avatar
Kim Nguyễn committed
28
29
30
31
32
33
34
35
36
37
38
39
40

% \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}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
41
42
43
44
45
46
47
\DeclareMathSymbol{\qm}{\mathalpha}{operators}{"3F}
\DeclareMathAlphabet{\mathbbm}{U}{bbold}{m}{n}
\newcommand{\dyn}{\ensuremath{\mathbbm%
    {\qm}}}
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\unk}{\texttt{?}}

Giuseppe Castagna's avatar
Giuseppe Castagna committed
48
\title{Intégration d'outils de programmation avancés dans un lagage avec types ensemblistes}
Kim Nguyễn's avatar
Kim Nguyễn committed
49
50

\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
51
52
\author{Proposants: Giuseppe Castagna, Kim Nguyen\\
Candidat: Mickaël Laurent}
Kim Nguyễn's avatar
Kim Nguyễn committed
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
90
91
92
93
94
95
\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
96
erreurs du programmeur qui essayerais de soustraire un tableau et une
Kim Nguyễn's avatar
Kim Nguyễn committed
97
98
99
100
101
102
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
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
110
complémentation, traditionnellement absents des langages de
Kim Nguyễn's avatar
Kim Nguyễn committed
111
112
113
114
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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
115
l'implémentation du langage CDuce \cite{BCF03}.
Kim Nguyễn's avatar
Kim Nguyễn committed
116
117
118
119
120
121
122
123
124
125










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

Giuseppe Castagna's avatar
Giuseppe Castagna committed
129
  \item typage d'occurrence
Kim Nguyễn's avatar
Kim Nguyễn committed
130

Giuseppe Castagna's avatar
Giuseppe Castagna committed
131
  \item types ensemblistes (types union, intersection et négation)
Kim Nguyễn's avatar
Kim Nguyễn committed
132

Giuseppe Castagna's avatar
Giuseppe Castagna committed
133
  \item typage graduel  et inférence de types
Kim Nguyễn's avatar
Kim Nguyễn committed
134

Giuseppe Castagna's avatar
Giuseppe Castagna committed
135
  \item polymorphisme paramétrique
Kim Nguyễn's avatar
Kim Nguyễn committed
136

Giuseppe Castagna's avatar
Giuseppe Castagna committed
137
  \item types récursifs
Giuseppe Castagna's avatar
Giuseppe Castagna committed
138
139
    
  \item effets et ordre supérieur
Kim Nguyễn's avatar
Kim Nguyễn committed
140

Giuseppe Castagna's avatar
Giuseppe Castagna committed
141
142
143
  \item raffinement de types  

\end{enumerate}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
144
Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
145

Giuseppe Castagna's avatar
Giuseppe Castagna committed
146
\paragraph{Typage d'occurrence:}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
147
148
Le typage de occurrence, ou \emph{occurrence typing}, est une technique
qui analyse les test effectués par un programme afin de pouvoir raffiner
Giuseppe Castagna's avatar
Giuseppe Castagna committed
149
150
l'analyses de types dans le code à exécuter en cas de réussite ou
d'échec du test. Un exemple d'application du typage d'occurrence est donné par le
Giuseppe Castagna's avatar
Giuseppe Castagna committed
151
code JavaScript suivant
Giuseppe Castagna's avatar
Giuseppe Castagna committed
152
153
154
155
156
\begin{alltt}
  function foo(x) {
      (typeof(x) === "number")? x++ : x.trim()
  }
\end{alltt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
157
Dans ce code on teste si l'argument liée à \code{x} de la fonction \code{foo} est de type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
158
159
160
\code{number}; si oui on renvoie le successeur de l'argument et si non
on lui envoie le message \code{trim()}. Puisque \code{trim} est une
méthode définie seulement pour les valeurs de type \code{string}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
161
(il s'agit d'une méthode du standard ECMAScript 5 qui élimines les espaces
Giuseppe Castagna's avatar
Giuseppe Castagna committed
162
163
au début et à la fin d'une chaine de caractères) on peut facilement
déduire que l'argument de \code{foo} doit être de type \code{number} ou
Giuseppe Castagna's avatar
Giuseppe Castagna committed
164
 \code{string}. C'est à dire il doit avoir le type ``union''
Giuseppe Castagna's avatar
Giuseppe Castagna committed
165
166
167
\code{number|string}. Dans les
systèmes de types standard  cette information n'est pas suffisante pour
pouvoir typer la fonction \code{foo} car
Giuseppe Castagna's avatar
Giuseppe Castagna committed
168
\code{trim()} n'est pas défini pour \code{number} (et donc pas pour un argument de type \code{number|string}) et \code{++} n'est
Giuseppe Castagna's avatar
Giuseppe Castagna committed
169
170
171
pas définie pour \code{string}. Ceci parce que les systèmes de types
standard ne prennent pas en compte le test de type effectué sur
\code{x}. Le typage d'occurrence est la technique qui utilise cette
Giuseppe Castagna's avatar
Giuseppe Castagna committed
172
information pour spécialiser le type des occurrences de \code{x} 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
173
de manière différente dans chaque branche du test: puisque le programme a testé que
Giuseppe Castagna's avatar
Giuseppe Castagna committed
174
\code{x} est de type \code{number}, alors nous pouvons supposer que
Giuseppe Castagna's avatar
Giuseppe Castagna committed
175
\code{x} est de type \code{number} dans la branche ``then'' du test, et
Giuseppe Castagna's avatar
Giuseppe Castagna committed
176
qu'il \emph{n'est pas} de type \code{number} dans la branche ``else''
Giuseppe Castagna's avatar
Giuseppe Castagna committed
177
178
(et de cela et du fait qu'il doit être ou \code{number} ou \code{string} déduire
qu'il est de type \code{string} dans cette branche).
Giuseppe Castagna's avatar
Giuseppe Castagna committed
179
180


Giuseppe Castagna's avatar
Giuseppe Castagna committed
181
182
183
184
Initialement défini pour le langage Scheme pour pouvoir typer des programmes
Scheme non typés~\cite{THF08,THF10}, le typage d'occurrence est de plus en plus étudié, développé
et utilisé dans l'industrie (en temoignent les langages Hack et Flow
développés par Facebook et  Typescript développé par Microsoft) car il est
Giuseppe Castagna's avatar
Giuseppe Castagna committed
185
indispensable pour pourvoir analyser des patterns de programmation
Giuseppe Castagna's avatar
Giuseppe Castagna committed
186
typiquement utilisés en programmation en langages dynamiques.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
187
188

\paragraph{Types ensemblistes:}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
189
comme nous venons de voir les types ensemblistes sont intimement liés
Giuseppe Castagna's avatar
Giuseppe Castagna committed
190
191
à l'occurrence typing. Le type que on déduira pour la fonction
\code{foo} sera \code{number|string $\to$ number|string}: une fonction
Giuseppe Castagna's avatar
Giuseppe Castagna committed
192
qui mappe un type union dans le même type union. Nous avons aussi déjà vu
Giuseppe Castagna's avatar
Giuseppe Castagna committed
193
l'utilisation du type négation: quand nous avons dit que dans la
Giuseppe Castagna's avatar
Giuseppe Castagna committed
194
195
196
197
198
199
200
201
202
203
branche ``else'' l'occurrence de \code{x} n'est pas de type
\code{number} cela signifie qu'elle est de type
\code{$\neg$number}. Et puisque \code{x} doit aussi avoir le type
\code{number|string} on déduit que cette occurrence aura
\emph{l'intersection} de deux types, c'est-à-dire
\code{(number|string)\&$\neg$number} =
\code{(number|string)$\setminus$number} = \code{string}. Mais on
pourrait aussi utiliser un type intersection pour donner un type bien
plus précis à \code{foo} tel
\code{(number$\to$number)\&(string$\to$string)} qui capture le fait
Giuseppe Castagna's avatar
Giuseppe Castagna committed
204
que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée
Giuseppe Castagna's avatar
Giuseppe Castagna committed
205
206
207
208
209
à une chaine de caractères renvoie une chaine de caractères. On parle
dans ce cas de polymorphisme ``ad hoc'', car
il permet de typer des fonctions surchargées (en anglais
\emph{overloaded functions}) qui executent du code different sur des
arguments de types différents. 
Giuseppe Castagna's avatar
Giuseppe Castagna committed
210
211
212
213
214
215
216

\paragraph{Typage graduel et inférence de types:}
nous avons déjà vous que une certaine dose de inférence de types est
nécessaire: la fonction \code{foo} n'a pas d'annotation de type mais
on veut déduire qu'elle est de type \code{number|string $\to$
  number|string} ou, ce qui est encore plus difficile à déduire, de
type \code{(number$\to$number)\&(string$\to$string)}. Si la première
Giuseppe Castagna's avatar
Giuseppe Castagna committed
217
déduction est déjà possible dans les systèmes actuels, la deuxième le sera surement grâce aux
Giuseppe Castagna's avatar
Giuseppe Castagna committed
218
219
techniques développés dans cette thèse. Toutefois une tel déduction
n'est pas toujours possible, c'est pourquoi il faudra avoir la
Giuseppe Castagna's avatar
Giuseppe Castagna committed
220
221
222
223
224
225
possibilité de mélanger des zones du programme typées statiquement avec
d'autres zones typées dynamiquement C'est exactement le but du \emph{typage graduel}
qui permet d'annoter certaines parties du programme par un type inconnu
\dyn, qui signale au compilateur que le typage statique peut être
relâche au cout d'un contrôle dynamique des types. Par exemple la
fonction \code{foo} pourrait être définie comme:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
226
227
228
229
230
\begin{alltt}
  function foo(x:\dyn) {
      (typeof(x) === "number")? x++ : x.trim()
  }
\end{alltt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
231
232
233
elle serait donc typée par \code{\dyn$\to$(number|string)} et le
compilateur introduirait des tests dynamiques qui contrôleraient à
l’exécution que lors de l’exécution de \code{x++} la variable est liée
Giuseppe Castagna's avatar
Giuseppe Castagna committed
234
235
à un entier et que lors de l'exécution de \code{x.trim()} la variable
est liée à une chaine de caractères.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
236
237


Giuseppe Castagna's avatar
Giuseppe Castagna committed
238
239
240
\paragraph{Polymorphisme paramétrique:} le polymorphisme paramétrique
est désormais un outil incontournable dans un langage de programmation moderne pour
pouvoir capturer ...
Giuseppe Castagna's avatar
Giuseppe Castagna committed
241

Giuseppe Castagna's avatar
Giuseppe Castagna committed
242
Un simple exemple de cette nécessitée peut être obtenu en
Giuseppe Castagna's avatar
Giuseppe Castagna committed
243
244
modifiant légèrement le code de \code{foo} de façon que la branche
``else'' renvoie l'argument inchangé:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
245
246
247
248
249
\begin{alltt}
  function foo(x) {
      (typeof(x) === "number")? x++ : x
  }
\end{alltt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
250
dans ce cas il est clair que \code{foo} renvoie toujours un résultat
Giuseppe Castagna's avatar
Giuseppe Castagna committed
251
252
qui a le même type que l'argument. Ceci est exprimé par le type
polymorphe $\forall\alpha.\alpha\to\alpha$. Mais il se peut que le
Giuseppe Castagna's avatar
Giuseppe Castagna committed
253
254
polymorphisme paramétrique doive se combiner avec les caractéristiques
précédentes. Si par exemple la branche ``then'' teste si l'argument est
Giuseppe Castagna's avatar
Giuseppe Castagna committed
255
256
257
258
259
260
égal à 42
\begin{alltt}
  function foo(x) {
      (typeof(x) === "number")? (x==42) : x
  }
\end{alltt}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
261
alors le type que on veut déduire pour cette fonction est:
Giuseppe Castagna's avatar
Giuseppe Castagna committed
262
263
264
$\forall\alpha.$\code{(number$\to$boolean)\&(($\alpha\setminus$number)$\to$($\alpha\setminus$number))}. Autrement
dit, si \code{foo} est appliqué à un entier alors il renvoie un
booléen, sinon s'il est applique à un type qui n'est pas \code{number}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
265
il renvoie un résultat du même type.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
266
267


Giuseppe Castagna's avatar
Giuseppe Castagna committed
268
269
270
271
272
273
274
\paragraph{Types récursifs, effets et ordre supérieur:}
comme le polymorphisme paramétrique, ainsi les types récursifs les
effets et les fonctions d'ordre supérieure sont 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
intégrer ces caractéristiques avec celle énoncées ci dessus.
[developper?]
Giuseppe Castagna's avatar
Giuseppe Castagna committed
275

Giuseppe Castagna's avatar
Giuseppe Castagna committed
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
\paragraph{Raffinement de types:}
nous avons déjà montré deux ex amples de raffinent de types: le typage
d'occurrence permet de raffiner le type des occurrence 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 proposition logique. Par exemple on voudrait
définir le type de nombre impair comme il suit $\texttt{Odd} = \{
x\in\texttt{Int}~|~x\mod 2 = 1\}$: \texttt{Odd} est 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 de 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
raffiner son type par $\{x\in t~|~e\}$ dans la branche ``then'' et
$\{x\in t~|~\neg e\}$ dans la branche ``else''.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
294

Giuseppe Castagna's avatar
Giuseppe Castagna committed
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316



  
\subsection{Objectifs}

La plupart de ces sujets ont été étudiés séparément et pour certains
on a étudié leur combinaison. Mais l’intégration de toutes ses
caractéristiques ensemble dans un langage unique pose de nouveaux
défis qui demandent non seulement des avances sur chaque de ses sujets
mais sur leur combinaison. L'inférence de types intersection pour le
fonctions nécessitera d'une analyse fine que sera fournie par le
typage des occurrence et une analyse de contrôle de flot que on
tachera d'intégrer avec cette dernière. Cette analyse pourra aussi
être utilisée pour al gestion des effets. Pour ces derniers nous
envisageons d'utiliser les travaux sur les effets algébriques en le
combinant avec l'expressivité logiques des types
ensemblistes L'inférence de type polymorphe sera basée sur la
génération d'ensemble de contraintes dont la solution utilisera les
types récursifs et les types ensemblistes. Le typage d'occurrence sera
utilisé pour optimiser la compilation de systèmes graduels afin de
réduire le nombre de contrôles dynamiques.
Kim Nguyễn's avatar
Kim Nguyễn committed
317
318
319
320




Kim Nguyễn's avatar
Kim Nguyễn committed
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338



\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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
339
effet, les langages de choix des analystes de données sont usuellement
Kim Nguyễn's avatar
Kim Nguyễn committed
340
341
342
343
344
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.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
345
Cette chaire, financée par une donation d'Oracle Labs. Il est prévu
Kim Nguyễn's avatar
Kim Nguyễn committed
346
347
348
349
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
350
351
352
353
354
355
356
\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
Giuseppe Castagna's avatar
Giuseppe Castagna committed
357
suffisamment modulaire pour être étendue avec d'autres aspects, un
Kim Nguyễn's avatar
Kim Nguyễn committed
358
359
360
361
362
363
364
365
366
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
Kim Nguyễn's avatar
Kim Nguyễn committed
367
368
369
370
371
372
373
374
375
376
jusqu'à présent jamais été étudiée. Elle pose des problèmes théoriques
(en particulier, la sûreté du typage avec occurrences repose sur une
notion  de « réduction parallèle » 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.

\bibliographystyle{unsrt}
\bibliography{main}
Kim Nguyễn's avatar
Kim Nguyễn committed
377
378
379
380
381
382
\end{document}

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