Browse Source

add CI, write contexte and problematique

zapashcanon 2 years ago
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 20
  2. 184
  3. 15
  4. 7
  5. 23
  6. 3
  7. 1
  8. 27


@ -0,0 +1,20 @@
image: debian/unstable
- biber
- fonts-linuxlibertine
- inkscape
- python3-pygments
- texlive-extra-utils
- texlive-fonts-extra
- texlive-lang-french
- texlive-xetex
- ec1f49cd-38dc-41d9-89f4-c3b6ecd7bcad # ssh deploy key
- build: |
ls main.pdf
- deploy: |
scp -o StrictHostKeyChecking=no -q main.pdf


@ -1,150 +1,36 @@
author = {Robin Milner},
title = {A theory of type polymorphism in programming},
journal = {Journal of Computer and System Sciences},
year = {1978},
volume = {17},
pages = {348--375}
author = {Jean-Christophe Filli\^atre},
title = {Deductive Program Verification},
year = 2011,
month = dec,
type = {Th\`{e}se d'habilitation},
school = {Universit{\'e} Paris-Sud},
type_publi = {these},
url = {},
x-equipes = {demons PROVAL},
x-type = {habilitation},
x-support = {rapport},
topics = {team, proval}
author = {Jean-Christophe Filli\^atre and Andrei Paskevich},
title = {Why3 --- Where Programs Meet Provers},
booktitle = {Proceedings of the 22nd European Symposium on Programming},
month = mar,
year = 2013,
volume = {7792},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Matthias Felleisen and Philippa Gardner},
pages = {125--128},
hal = {},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {ESOP},
x-editorial-board = {yes},
x-international-audience = {yes}
hal = {},
author = {Martin Clochard and Jean-Christophe
Filli\^atre and Andrei Paskevich},
title = {How to avoid proving the absence of integer overflows},
pages = {94--109},
crossref = {vstte15},
topics = {team,lri},
keywords = {Why3},
type_publi = {icolcomlec},
x-international-audience = {yes},
x-proceedings = {yes}
topics = {team},
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {A Pragmatic Type System for Deductive Verification},
type = {Research Report},
institution = {Universit\'e Paris Sud},
year = 2016,
abstract = { In the context of deductive verication, it is customary
today to handle programs with pointers using either
separation logic, dynamic frames, or explicit memory
models. Yet we can observe that in numerous
programs, a large amount of code is within the scope
of Hoare logic, provided we can statically control
aliasing. When this is the case, the code
correctness can be reduced to simpler verication
conditions which do not require any explicit memory
model. This makes verication conditions more
amenable both to automated theorem proving and to
manual inspection and debugging. In this paper, we
devise a method of such static aliasing control for
a programming language featuring nested data
structures with mutable components. Our solution is
based on a type system with singleton regions and
eects, which we prove to be sound.},
hal = {},
note = {\url{}}
author = {Jean-Christophe Filli\^atre and L\'eon
Gondelman and Andrei Paskevich},
title = {The Spirit of Ghost Code},
journal = {Formal Methods in System Design},
publisher = {Springer},
year = 2016,
volume = 48,
number = 3,
pages = {152--174},
issn = {1572-8102},
doi = {10.1007/s10703-016-0243-x},
topics = {team},
hal = {},
keywords = {Why3},
type_publi = {irevcomlec},
x-international-audience = {yes},
x-proceedings = {yes},
x-type = {article},
x-support = {revue},
x-editorial-board = {yes},
abstract = {
In the context of deductive program verification, ghost code is part
of the program that is added for the purpose of specification.
Ghost code must not interfere with regular code, in the sense that
it can be erased without observable difference in the program outcome.
In particular, ghost data cannot participate in regular
computations and ghost code cannot mutate regular data or diverge.
The idea exists in the folklore since the early notion of auxiliary
variables and is implemented in many state-of-the-art program
verification tools. However, a rigorous definition and treatment of
ghost code is surprisingly subtle and few formalizations exist.
In this article, we describe a simple ML-style programming language
with mutable state and ghost code. Non-interference is ensured by a
type system with effects, which allows, notably, the same data types
and functions to be used in both regular and ghost code.
We define the procedure of ghost code erasure and we prove its
safety using bisimulation.
A similar type system, with numerous extensions which we briefly discuss,
is implemented in the program verification environment Why3.
author = {Jean-Christophe Filli{\^a}tre and L{\'e}on Gondelman and
Andrei Paskevich and M{\'a}rio Pereira and Sim{\~a}o Melo de Sousa},
title = {A Toolchain to {P}roduce {C}orrect-by-{C}onstruction {OC}aml
hal = {},
pdf = {},
note = {artifact: \url{}},
year = {2018}
title = {Document de présentation des algorithmes de Parcoursup},
year = 2019,
url = {}
ISSN = {00029947},
author = {H. G. Rice},
journal = {Transactions of the American Mathematical Society},
number = {2},
pages = {358--366},
publisher = {American Mathematical Society},
title = {Classes of Recursively Enumerable Sets and Their Decision Problems},
volume = {74},
year = {1953}
author="Moyen, Jean-Yves
and Simonsen, Jakob Grue",
editor="Manea, Florin
and Martin, Barnaby
and Paulusma, Dani{\"e}l
and Primiero, Giuseppe",
title="More Intensional Versions of Rice's Theorem",
booktitle="Computing with Foresight and Industry",
publisher="Springer International Publishing",
abstract="Classic results in computability theory concern extensional results: the behaviour of partial recursive functions rather than the programs computing them. We prove a generalisation of Rice's Theorem concerning equivalence classes of programs and show how it can be used to study intensional properties such as time and space complexity. While many results that follow from our general theorems can - and have - been proved by more involved, specialised methods, our results are sufficiently simple that little work is needed to apply them.",
author = {Henrik Reif Andersen},
title = {An Introduction to Binary Decision Diagrams},
howpublished = {Lectures notes from Technical University of Denmark},
year = 1997,
note = {\url{}}


@ -0,0 +1,15 @@
\section{Contexte du stage}
\subsection{L'Université Paris-Saclay}
Ce stage s'inscrit dans le dans le cadre de ma formation en Master 2 \emph{Fondements de l'Informatique et Ingénierie du Logiciel} à l'\href{}{Université Paris-Saclay}. Il m'était demandé d'effectuer un stage de six mois en entreprise ou bien dans un laboratoire de recherche. Dans une optique de diversification, d'ouverture au monde et ayant choisi pour mes quatre précédents stages un laboratoire de recherche public, j'ai fait cette fois-ci le choix d'un stage en entreprise mais toujours sur un sujet de recherche.
\paragraph{L'entreprise} Mon stage s'est déroulé au sein d'\href{}{OCamlPro} ; une entreprise qui, comme son nom l'indique, utilise principalement le langage \href{}{OCaml} et est composée d'environ une vingtaine de personnes.
\paragraph{Expertise} L'entreprise est spécialisée dans le prototypage et le développement de logiciels en OCaml, les méthodes formelles et le développement de langages de programmation. Quelques exemples sont \href{}{opam}, \href{}{alt-ergo} et \href{}{flambda}. D'autre part, OCamlPro dispense aussi des formations et a contribué à l'écriture de cours en ligne, notamment sur OCaml et Rust.
\paragraph{L'équipe compilation} J'ai été encadré par Pierre \bsc{Chambart} qui est directeur de la technologie\footnote{Ou \emph{Chief Technology Officer} en anglais.} et ingénieur recherche et développement senior. Il fait partie de l'équipe compilation au sein de laquelle il travaille sur le compilateur OCaml et notamment sur son futur \emph{inliner} : flambda2. Précédemment, l'équipe a publié flambda qui est disponible comme une variante du compilateur OCaml.
\paragraph{Motivation du choix} Je souhaitais un sujet de stage portant sur le design et l'implémentation des langages de programmation et où il me serait possible de programmer en OCaml, qui est un langage avec lequel j'ai de fortes affinités et qui est très certainement mon langage favori. OCamlPro m'a donc semblé un choix naturel et évident. J'ai contacté Pierre, que j'avais déjà rencontré par le passé, en lui proposant un sujet que j'avais moi-même écrit. Il m'a donné rendez-vous le lendemain dans les locaux d'OCamlPro et a accepté de m'encadrer. Ainsi débute cette aventure\ldots{}


@ -14,15 +14,18 @@


@ -0,0 +1,23 @@
let rec list_length_a = function
| [] -> 0
| _::s -> 1 + (list_length_a s)
let list_length_b =
let rec aux acc = function
| [] -> acc
| _::s -> aux (acc + 1) s
aux 0
let rec list_length_c =
let length = ref 0 in
| [] -> let res = !length in length := 0; res
| _::s -> incr length; list_length_c s
let () =
let l = ['a'; 'b'; 'c'] in
assert (list_length_a l = 3);
assert (list_length_b l = 3);
assert (list_length_c l = 3);
Format.printf "OK !@."


@ -1,3 +0,0 @@


@ -1 +0,0 @@
\section{Le problème}


@ -0,0 +1,27 @@
\subsection{Un résultat, plusieurs programmes}
\paragraph{Exemple mathématique} Il est très facile d'écrire deux expressions mathématiques équivalentes de plusieurs façons différentes. L'expression $2 + 2$ est bien évidemment équivalente à $4$ et à $1 + 1 + 1 + 1$.
\paragraph{Exemple informatique} Il en va de même pour les programmes informatiques. En OCaml, par exemple, on peut écrire la fonction qui calcule la longueur d'une liste d'au moins trois façons\footnote{Et très certainement de beaucoup d'autres.} :
\paragraph{Problème} Cela pose plusieurs problèmes. Par exemple, dans un programme contenant des millions de lignes et écrit par plusieurs personnes, il peut arriver que l'on écrive plusieurs fois des fonctions équivalentes. On parle de duplication de code. Le programme prend alors plus de place que nécessaire et est plus difficile à maintenir.
\paragraph{Réusinage} Lorsqu'un programmeur réalise qu'un programme contient deux fonctions équivalentes, il peut alors procéder à un réusinage\footnote{Ou \emph{refactoring} en anglais.} afin de n'avoir plus qu'une seule version de cette fonction. Seulement, c'est un processus long et coûteux.
\paragraph{Objectif} On aimerait donc pouvoir détecter automatiquement l'équivalence extensionnelle de deux programmes\footnote{Ou plutôt de deux fonctions, ce qui revient au même.} afin d'éviter la duplication de code et de faciliter le réusinage.
\subsection{Indécidabilité de l'équivalence extensionnelle}
\paragraph{Équivalence extensionnelle} La relation entre deux programmes qui \emph{calculent la même chose} est appelée l'\emph{équivalence extensionnelle}.
\paragraph{Indécidabilité} Malheureusement, le théorème de Rice\cite{Rice53} implique l'indécidabilité de l'équivalence extensionnelle\cite{MoyenSimonsen19}. C'est-à-dire qu'il est impossible d'écrire un programme qui détecte si deux programmes sont équivalents.
\paragraph{Piste de solution} Seulement, ce théorème se place dans le cadre de programmes écrits dans un langage Turing-complet. On peut donc espérer arriver à décider l'équivalence extensionnelle dans un langage qui ne serait pas Turing-complet. La difficulté réside alors dans le fait de conserver un langage qui permette à la fois de calculer des choses \emph{intéressantes} et qui reste suffisamment expressif pour être agréable à utiliser.
\subsection{Sujet de stage initial et évolution}
L'objectif initial du stage était donc de développer un langage de programmation dans lequel on détecterait l'équivalence extensionnelle au moyen de structures de données telles que les diagrammes de décision binaires\cite{Andersen97} et des généralisations de ceux-ci. Finalement, il a plutôt été question de développer des formes canoniques sur le langage et de forcer le programmeur à les utiliser : il n'est a priori pas aberrant de penser que moins il y a de façons valables d'écrire un programme qui calcule un résultat, plus il est plus facile de décider l'équivalence extensionnelle.