hms/web
1
0
Fork 0
Code Activity Actions

feat: both english and french versions

Browse source
This commit is contained in:
Henri Saudubray 2025-10-20 10:50:54 +02:00
parent 1703b80353
commit 770c75593e
Signed by: hms
GPG key ID: 7065F57ED8856128
10 changed files with 743 additions and 341 deletions
Download patch file Download diff file Expand all files Collapse all files

163
man.html
View file

@ -1,11 +1,11 @@
<!DOCTYPE html>
<html lang="en">
<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="Computer Science Student">
<meta name="description" content="Doctorant en m&#xE9;thodes formelles">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
</head>
<body>
@ -17,22 +17,24 @@
</div>
<header>
<span>HENRI(1)</span>
<span>User information</span>
<span>Informations utilisateur</span>
<span>HENRI(1)</span>
</header>
<main>
<div class="section" id="name">
<div class="section-title">Name</div>
<div class="section-title">Nom</div>
<div class="content">
Henri Saudubray - PhD student
Henri Saudubray - Doctorant en M&#xE9;thodes Formelles
</div>
</div>
<div class="section" id="synopsis">
<div class="section-title">Synopsis</div>
<div class="content">
I am a PhD student at Laboratoire M&#xE9;thodes Formelles (LMF) at
Universit&#xE9; Paris Saclay, focusing on formal logic, proof
assistants, and programming languages.
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">
@ -46,117 +48,127 @@
<div class="description">
"Faire chauffer Why3 avec de l'induction".
<br>
Describes the addition of a new construct to the WhyML language
allowing for case analysis on inductive predicate instances.
D&#xE9;crit l'ajout d'une nouvelle construction au langage WhyML
permettant le filtrage sur les instances de pr&#xE9;dicats
inductifs.
<br>
Written with <a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filliâtre</a>
and <a href="http://www.tertium.org/">Andrei Paskevich</a>.
&#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">Experience</div>
<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>
- Since October 2025
- Depuis octobre 2025
</div>
<div class="description">
PhD, with <a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filliâtre</a>
and <a href="http://www.tertium.org/">Andrei Paskevich</a>.
Working on the design and unification of programming,
specification and proof languages in the context of deductive
program verification, in the
<a href="https://www.why3.org">Why3</a> platform.
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>
- March to August 2025
- Mars - ao&#xFB;t 2025
</div>
<div class="description">
M2 Internship, with <a href="https://www.di.ens.fr/~pouzet/">
Marc Pouzet</a>. Worked on reproducibility and transparency of
assertions in the synchronous hybrid language
<a href="https://zelus.di.ens.fr">Z&#xE9;lus</a>.
Designed and implemented a
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">
formal executable semantics</a> for a multi-solver language
runtime.
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>
- March to July 2024
- Mars - juillet 2024
</div>
<div class="description">
M1 Internship, with
Stage de M1, encadr&#xE9; par
<a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filliâtre</a>
and <a href="http://www.tertium.org">Andrei Paskevich</a>.
Added support for case analysis and proofs by
induction on inductive predicates in the
<a href="https://www.why3.org">Why3</a> platform.
Translated a <a href="https://codeberg.org/17maiga/lambda">
Coq proof to Why3</a> as a test.
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>
- September 2022 to August 2023
<a href="https://skapane.ai">Skap&#xE1;n&#xEA;</a> - Septembre
2022 - ao&#xFB;t 2023
</div>
<div class="description">
L3 Traineeship. Back-end development on containerized
infrastructure in Python. Web app design with React.js, Flask and
Docker.
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>
- May to August 2022
- Mai - ao&#xFB;t 2022
</div>
<div class="description">
L2 Internship. Development of an automated end-to-end testing tool
and ISO 20022 file format converter for CDC's banking
infrastructure in Java.
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 - August 2021 - May 2022</div>
<div class="title">Ac'Lab - Ao&#xFB;t 2021 - mai 2022</div>
<div class="description">
Association. Vice-Treasurer and Teaching Lead.
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>
- May to August 2021
<a href="https://www.fnacdarty.com">Fnac Darty</a> - Mai -
ao&#xFB;t 2021
</div>
<div class="description">
L1 Internship. Work on customer insight and customer journey.
Deployment of an in-house iOS application.
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">Education</div>
<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>
- September 2024 - March 2025
<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)
@ -165,8 +177,8 @@
<li>
<div class="title">
<a href="https://www.sciences.universite-paris-saclay.fr">
Facult&#xE9; des Sciences - Universit&#xE9; Paris Saclay</a>
- September 2023 - March 2024
Facult&#xE9; des Sciences - Universit&#xE9; Paris-Saclay</a>
- Septembre 2023 - mars 2024
</div>
<div class="description">
Master Parisien de Recherche en Informatique (MPRI)
@ -174,9 +186,8 @@
</li>
<li>
<div class="title">
<a href="https://www.fges.fr"
>FGES - Universit&#xE9; Catholique de Lille</a>
- September 2020 to May 2023
<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)
@ -185,43 +196,40 @@
</ul>
</div>
<div class="section" id="files">
<div class="section-title">Files</div>
<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="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">Report for M1 Internship.</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">Report for M2 Internship.</div>
<div class="description">Rapport de stage de M2.</div>
</li>
</ul>
</div>
<div class="section" id="see_also">
<div class="section-title">See Also</div>
<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>
<a href="mailto:hms@lmf.cnrs.fr">hms[at]lmf[dot]cnrs[dot]fr</a>
</div>
<div class="description">Email address.</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">Git forge.</div>
<div class="description">Forge git.</div>
</li>
<li>
<div class="title">
@ -232,10 +240,13 @@
</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.0</span>
<span>2025-10-03&nbsp;</span>
<span>1.5.1</span>
<span>2025-10-20&nbsp;</span>
<span>HENRI(1)</span>
</footer>
</body>