diff --git a/man.html b/man.html index 48ca588..abca4e0 100644 --- a/man.html +++ b/man.html @@ -41,8 +41,7 @@
  • - /pdf/articles/jfla-2025.pdf - + /pdf/articles/jfla-2025.pdf
    "Faire chauffer Why3 avec de l'induction". @@ -51,8 +50,8 @@ allowing for case analysis on inductive predicate instances.
    Written with - Jean-Christophe Filliâtre - and Andrei Paskevich. + Jean-Christophe Filliâtre + and Andrei Paskevich.
  • @@ -68,7 +67,10 @@ - Since October 2025
    - PhD. Working on the design and unification of programming, + PhD, with + Jean-Christophe Filliâtre + and Andrei Paskevich. + Working on the design and unification of programming, specification and proof languages in the context of deductive program verification, in the Why3 platform. @@ -80,13 +82,14 @@ - March to August 2025
    - M2 Internship. Worked on reproducibility and transparency of + M2 Internship, with + Marc Pouzet. Worked on reproducibility and transparency of assertions in the synchronous hybrid language Zélus. Designed and implemented a - formal executable semantics - for a multi-solver language runtime. + formal executable semantics for a multi-solver language + runtime.
  • @@ -96,7 +99,11 @@ - March to July 2024
    - M1 Internship. Added support for case analysis and proofs by + M1 Internship, with + + Jean-Christophe Filliâtre + and Andrei Paskevich. + Added support for case analysis and proofs by induction on inductive predicates in the Why3 platform. Translated a @@ -227,7 +234,7 @@