hms/web
1
0
Fork 0
Code Activity Actions
web/man.html

253 lines
9.8 KiB
HTML
Raw Blame History

<!DOCTYPE html>
<html lang="fr">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<link rel="stylesheet" type="text/css" href="./css/base.css?version=3">
<link rel="stylesheet" type="text/css" href="./css/man.css?version=3">
<title>Henri Saudubray</title>
<meta name="description" content="Doctorant en m&#xE9;thodes formelles">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
</head>
<body>
<div id="pride-banner">
<div class="color yellow"></div>
<div class="color white"></div>
<div class="color purple"></div>
<div class="color black"></div>
</div>
<header>
<span>HENRI(1)</span>
<span>Informations utilisateur</span>
<span>HENRI(1)</span>
</header>
<main>
<div class="section" id="name">
<div class="section-title">Nom</div>
<div class="content">
Henri Saudubray - Doctorant en M&#xE9;thodes Formelles
</div>
</div>
<div class="section" id="synopsis">
<div class="section-title">Synopsis</div>
<div class="content">
Je suis doctorant au Laboratoire M&#xE9;thodes Formelles
(LMF) de l'Universit&#xE9; Paris-Saclay. Je m'int&#xE9;resse
&#xE0; l'&#xE9;tude des langages de programmation, &#xE0; la
v&#xE9;rification d&#xE9;ductive, aux assistants de preuve, et &#xE0;
la logique formelle.
</div>
</div>
<div class="publications" id="publications">
<div class="section-title">Publications</div>
<ul class="content">
<li>
<div class="title">
<a href="./pdf/articles/jfla-2025.pdf">
/pdf/articles/jfla-2025.pdf</a>
</div>
<div class="description">
"Faire chauffer Why3 avec de l'induction".
<br>
D&#xE9;crit l'ajout d'une nouvelle construction au langage WhyML
permettant le filtrage sur les instances de pr&#xE9;dicats
inductifs.
<br>
&#xE9;crit avec
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filli&#xE2;tre</a>
et <a href="http://www.tertium.org/">Andrei Paskevich</a>.
</div>
</li>
</ul>
</div>
<div class="section" id="experience">
<div class="section-title">Exp&#xE9;rience</div>
<ul class="content">
<li>
<div class="title">
<a href="https://lmf.cnrs.fr">
Laboratoire M&#xE9;thodes Formelles,
Universit&#xE9; Paris-Saclay</a>
- Depuis octobre 2025
</div>
<div class="description">
Doctorat, encadr&#xE9; par
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filli&#xE2;tre</a>
et <a href="http://www.tertium.org/">Andrei Paskevich</a>.
Conception et unification des langages de programmation,
sp&#xE9;cification et preuve dans le contexte de la
v&#xE9;rification d&#xE9;ductive de programmes, au sein de l'outil
<a href="https://www.why3.org">Why3</a>.
</div>
</li>
<li>
<div class="title">
<a href="https://parkas.di.ens.fr">
INRIA, PARKAS Team</a>
- Mars - ao&#xFB;t 2025
</div>
<div class="description">
Stage de M2, encadr&#xE9; par
<a href="https://www.di.ens.fr/~pouzet/">Marc Pouzet</a>. Travail
autour de la reproductibilit&#xE9; et de la transparence des
assertions ex&#xE9;cutables dans le langage hybride
<a href="https://zelus.di.ens.fr">Z&#xE9;lus</a>. Conception et
impl&#xE9;mentation d'une
<a href="https://codeberg.org/17maiga/hsim">
s&#xE9;mantique ex&#xE9;cutable</a> pour un environnement
d'ex&#xE9;cution multi-solveur.
</div>
</li>
<li>
<div class="title">
<a href="https://lmf.cnrs.fr">
Laboratoire M&#xE9;thodes Formelles, CNRS</a>
- Mars - juillet 2024
</div>
<div class="description">
Stage de M1, encadr&#xE9; par
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filli&#xE2;tre</a>
et <a href="http://www.tertium.org">Andrei Paskevich</a>.
Ajout d'une nouvelle construction au langage WhyML permettant le
filtr&#xE2;ge sur les instances de pr&#xE9;dicats inductifs au
sein de l'outil <a href="https://www.why3.org">Why3</a>.
Traduction d'une <a href="https://codeberg.org/17maiga/lambda">
preuve Rocq vers Why3</a> comme exemple d'utilisation.
</div>
</li>
<li>
<div class="title">
<a href="https://skapane.ai">Skap&#xE1;n&#xEA;</a> - Septembre
2022 - ao&#xFB;t 2023
</div>
<div class="description">
Alternance en L3. D&#xE9;veloppement back-end sur une
infrastructure conteneuris&#xE9;e en Python et Scala. Conception
d'une plateforme de gestion d'environnements de d&#xE9;veloppement
Jupyter avec React.js, Flask et Docker.
</div>
</li>
<li>
<div class="title">
<a href="https://www.icdc.caissedesdepots.fr">Informatique CDC</a>
- Mai - ao&#xFB;t 2022
</div>
<div class="description">
Stage de L2. D&#xE9;veloppement en Java d'un outil
d'automatisation de tests bout en bout et d'un convertisseur de
fichiers ISO 20022 sur l'infrastructure banquaire de la Caisse des
D&#xE9;p&#xF4;ts et Consignations.
</div>
</li>
<li>
<div class="title">Ac'Lab - Ao&#xFB;t 2021 - mai 2022</div>
<div class="description">
Engagement associatif au sein de l'association d'informatique de
la facult&#xE9;. Vice-tr&#xE9;sorier et responsable enseignement.
Organisation d'&#xE9;v&#xE9;nements, enseignement des bases du
langage Python, gestion de budget.
</div>
</li>
<li>
<div class="title">
<a href="https://www.fnacdarty.com">Fnac Darty</a> - Mai -
ao&#xFB;t 2021
</div>
<div class="description">
Stage de L1. Travail sur le parcours utilisateur sur les sites
e-commerce de Fnac et Darty. D&#xE9;ploiement d'une application
iOS interne.
</div>
</ul>
</div>
<div class="section" id="education">
<div class="section-title">&#xE9;ducation</div>
<ul class="content">
<li>
<div class="title">
<a href="https://ens-paris-saclay.fr">ENS Paris-Saclay</a> -
Septembre 2024 - mars 2025
</div>
<div class="description">
Master Parisien de Recherche en Informatique (MPRI)
</div>
</li>
<li>
<div class="title">
<a href="https://www.sciences.universite-paris-saclay.fr">
Facult&#xE9; des Sciences - Universit&#xE9; Paris-Saclay</a>
- Septembre 2023 - mars 2024
</div>
<div class="description">
Master Parisien de Recherche en Informatique (MPRI)
</div>
</li>
<li>
<div class="title">
<a href="https://www.fges.fr">FGES - Universit&#xE9; Catholique de
Lille</a> - Septembre 2020 - mai 2023
</div>
<div class="description">
Licence Sciences du Num&#xE9;rique (SDN)
</div>
</li>
</ul>
</div>
<div class="section" id="files">
<div class="section-title">Fichiers</div>
<ul class="content">
<li>
<div class="title"><a href="./pdf/cv.pdf">/pdf/cv.pdf</a></div>
<div class="description">Curriculum Vitae.</div>
</li>
<li>
<div class="title">
<a href="./pdf/m1_report.pdf">/pdf/m1_report.pdf</a>
</div>
<div class="description">Rapport de stage de M1.</div>
</li>
<li>
<div class="title">
<a href="./pdf/m2_report.pdf">/pdf/m2_report.pdf</a>
</div>
<div class="description">Rapport de stage de M2.</div>
</li>
</ul>
</div>
<div class="section" id="see_also">
<div class="section-title">Liens annexes</div>
<ul class="content">
<li>
<div class="title">
<a href="mailto:hms@lmf.cnrs.fr">hms[at]lmf[dot]cnrs[dot]fr</a>
</div>
<div class="description">Email.</div>
</li>
<li>
<div class="title">
<a href="https://codeberg.org/17maiga">codeberg.org/17maiga</a>
</div>
<div class="description">Forge git.</div>
</li>
<li>
<div class="title">
<a href="https://linkedin.com/in/henri-saudubray"
>linkedin.com/in/henri-saudubray</a>
</div>
<div class="description">LinkedIn.</div>
</li>
</ul>
</div>
<div class="section" id="utils">
<a href="man.en.html">Read this page in english</a>
</div>
</main>
<footer>
<span>1.5.1</span>
<span>2025-10-20&nbsp;</span>
<span>HENRI(1)</span>
</footer>
</body>
</html>
View git blame Copy permalink