1
0
Fork 0

feat: add advisors in internships and phd

This commit is contained in:
Henri Saudubray 2025-10-03 17:33:59 +02:00
parent 0aaa689ca2
commit 4ab4f3f363
Signed by: hms
GPG key ID: 7065F57ED8856128

View file

@ -41,8 +41,7 @@
<li> <li>
<div class="title"> <div class="title">
<a href="./pdf/articles/jfla-2025.pdf"> <a href="./pdf/articles/jfla-2025.pdf">
/pdf/articles/jfla-2025.pdf /pdf/articles/jfla-2025.pdf</a>
</a>
</div> </div>
<div class="description"> <div class="description">
"Faire chauffer Why3 avec de l'induction". "Faire chauffer Why3 avec de l'induction".
@ -51,8 +50,8 @@
allowing for case analysis on inductive predicate instances. allowing for case analysis on inductive predicate instances.
<br> <br>
Written with <a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html"> Written with <a href="https://usr.lmf.cnrs.fr/~jcf/index.fr.html">
Jean-Christophe Filliâtre Jean-Christophe Filliâtre</a>
</a> and <a href="http://www.tertium.org/">Andrei Paskevich</a>. and <a href="http://www.tertium.org/">Andrei Paskevich</a>.
</div> </div>
</li> </li>
</ul> </ul>
@ -68,7 +67,10 @@
- Since October 2025 - Since October 2025
</div> </div>
<div class="description"> <div class="description">
PhD. Working on the design and unification of programming, 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 specification and proof languages in the context of deductive
program verification, in the program verification, in the
<a href="https://www.why3.org">Why3</a> platform. <a href="https://www.why3.org">Why3</a> platform.
@ -80,13 +82,14 @@
- March to August 2025 - March to August 2025
</div> </div>
<div class="description"> <div class="description">
M2 Internship. Worked on reproducibility and transparency of 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 assertions in the synchronous hybrid language
<a href="https://zelus.di.ens.fr">Z&#xE9;lus</a>. <a href="https://zelus.di.ens.fr">Z&#xE9;lus</a>.
Designed and implemented a Designed and implemented a
<a href="https://codeberg.org/17maiga/hsim"> <a href="https://codeberg.org/17maiga/hsim">
formal executable semantics formal executable semantics</a> for a multi-solver language
</a> for a multi-solver language runtime. runtime.
</div> </div>
</li> </li>
<li> <li>
@ -96,7 +99,11 @@
- March to July 2024 - March to July 2024
</div> </div>
<div class="description"> <div class="description">
M1 Internship. Added support for case analysis and proofs by M1 Internship, 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>.
Added support for case analysis and proofs by
induction on inductive predicates in the induction on inductive predicates in the
<a href="https://www.why3.org">Why3</a> platform. <a href="https://www.why3.org">Why3</a> platform.
Translated a <a href="https://codeberg.org/17maiga/lambda"> Translated a <a href="https://codeberg.org/17maiga/lambda">
@ -227,7 +234,7 @@
</div> </div>
</main> </main>
<footer> <footer>
<span>1.4.1</span> <span>1.5.0</span>
<span>2025-10-03&nbsp;</span> <span>2025-10-03&nbsp;</span>
<span>HENRI(1)</span> <span>HENRI(1)</span>
</footer> </footer>