Commit 623be6ab authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added title

parent 61c4ba05
......@@ -27,3 +27,84 @@
biburl = {https://dblp.org/rec/journals/acs/PlotkinP03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{THF10,
author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
title = {Logical types for untyped languages},
booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
series = {{ICFP} '10},
year = {2010},
isbn = {978-1-60558-794-3},
location = {Baltimore, Maryland, {USA}},
pages = {117--128},
numpages = {12},
url = {http://doi.acm.org/10.1145/1863543.1863561},
doi = {10.1145/1863543.1863561},
acmid = {1863561},
publisher = {{ACM}},
address = {New York, NY, {USA}},
keywords = {logic, type systems, untyped languages},
}
@INPROCEEDINGS{BCF03,
AUTHOR = {V\'eronique Benzaken and Giuseppe Castagna and Alain Frisch},
TITLE = {{CD}uce: an {XML}-Centric General-Purpose Language},
BOOKTITLE = {ICFP~'03, 8th ACM International Conference on Functional Programming},
url = {http://doi.acm.org/10.1145/944746.944711},
PAGES ={51--63},
ADDRESS = {Uppsala, Sweden},
DMI-CATEGORY = {intc},
PUBLISHER = {ACM Press},
YEAR = {2003},
}
@Manual{typescript,
title = {{TypeScript}},
url = {https://www.typescriptlang.org/},
organization = {Microsoft},
year = {\mbox{\!}}
}
@Manual{Flow,
title = {{Flow}},
url = {https://flow.org/},
organization = {Facebook},
year = {\mbox{\!}}}
}
@inproceedings{THF08,
author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
title = {The Design and Implementation of Typed Scheme},
booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
series = {POPL '08},
year = {2008},
isbn = {978-1-59593-689-9},
location = {San Francisco, California, USA},
pages = {395--406},
numpages = {12},
url = {http://doi.acm.org/10.1145/1328438.1328486},
doi = {10.1145/1328438.1328486},
acmid = {1328486},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {scheme, type systems},
}
@article{Frisch2008,
author = {Frisch, Alain and Castagna, Giuseppe and Benzaken, V{\'e}ronique},
title = {Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types},
journal = {Journal of the {ACM}},
issue_date = {September 2008},
volume = {55},
number = {4},
month = sep,
year = {2008},
issn = {0004-5411},
pages = {19:1--19:64},
url = {http://doi.acm.org/10.1145/1391289.1391293},
publisher = {{ACM}},
}
\ No newline at end of file
......@@ -45,10 +45,11 @@
\newcommand{\code}[1]{\texttt{#1}}
\newcommand{\unk}{\texttt{?}}
\title{...}
\title{Intégration d'outils de programmation avancés dans un lagage avec types ensemblistes}
\subtitle{Sujet de thèse} % \\ {\small\emph{DRAFT, please do not distribute}}}
\author{Giuseppe Castagna, Kim Nguyen}
\author{Proposants: Giuseppe Castagna, Kim Nguyen\\
Candidat: Mickaël Laurent}
\date{\today}
\begin{document}
......@@ -106,12 +107,12 @@ 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
complémentation, traditionnellement absents 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{}.
l'implémentation du langage CDuce \cite{BCF03}.
......@@ -122,7 +123,7 @@ l'implantation du langage CDuce \cite{}.
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 avancée suivantes:
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:
\begin{enumerate}
\item typage d'occurrence
......@@ -143,51 +144,52 @@ Le but de cette thèse est d'arriver à définir et étudier un langage de progr
Nous allons montrer par des exemples l'intérêt de chaque caractéristique:
\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
Le typage de occurrence, ou \emph{occurrence typing}, est une technique
qui analyse les test effectués par un programme afin de pouvoir raffiner
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
code suivant JavaScript
code JavaScript suivant
\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} est de type
Dans ce code on teste si l'argument liée à \code{x} de la fonction \code{foo} est de type
\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}
(c'est une méthode du standard ECMAScript 5 qui élimines les espaces
(il s'agit d'une méthode du standard ECMAScript 5 qui élimines les espaces
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
\code{string}. C'est à dire il doit avoir le type
\code{string}. C'est à dire il doit avoir le type ``union''
\code{number|string}. Dans les
systèmes de types standard cette information n'est pas suffisante pour
pouvoir typer la fonction \code{foo} car
\code{trim()} n'est pas défini pour \code{number} et \code{++} n'est
\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
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
information pour spécialiser le type des occurrences de \code{x} dans
information pour spécialiser le type des occurrences de \code{x}
de manière différente dans chaque branche du test: puisque le programme a testé que
\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 du fait qu'il doit être ou \code{number} ou \code{string} déduire
qu'il est de type \code{string} dans cette branche.
(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).
Initialement défini pour le langage Scheme pour pouvoir typer des programme
Scheme non typés\cite{THF08,THF10}, il est de plus en plus développé
et utilisé dans l'industrie (Hack, Typescript, Flow) car il est
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
indispensable pour pourvoir analyser des patterns de programmation
typiquement utilisé en programmation par des langages dynamiques.
typiquement utilisés en programmation en langages dynamiques.
\paragraph{Types ensemblistes:}
comme nous venons de voir les types ensemblistes sont intimement liés
à l'occurrence typing. Le type que on déduira pour la fonction
\code{foo} sera \code{number|string $\to$ number|string}: une fonction
qui mappe un type union dans un type union. Nous avons aussi déjà vu
qui mappe un type union dans le même type union. Nous avons aussi déjà vu
l'utilisation du type négation: quand nous avons dit que dans la
branche ``else'' l'occurrence de \code{x} n'est pas de type
\code{number} cela signifie qu'elle est de type
......@@ -200,7 +202,11 @@ 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
que \code{foo} appliquée à un entier renvoie un entier et qu'appliquée
à une chaine de caractères renvoie une chaine de caractères.
à 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.
\paragraph{Typage graduel et inférence de types:}
nous avons déjà vous que une certaine dose de inférence de types est
......
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