Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision 		Révision précédente
Prochaine révision Les deux révisions suivantes
fr:research:models-computation [2021/04/05 17:50]
apeiron 		fr:research:models-computation [2021/04/05 18:00]
apeiron
Ligne 1: Ligne 1:
 +Durant ma thèse j'ai prouvé des équivalences entre modèles de calcul en utilisant une simulation mutuelle, mettant en pratique l'​identité des indiscernables.
 +J'ai caractérisé des classes temporelles d'​algorithmes en utilisant des restrictions syntaxiques sur les langages de programmation impératifs,​ garantissant ainsi la complexité implicite des codes développés.
 +Durant mon premier postdoc j'ai utilisé les automates cellulaires pour mieux comprendre la propagation de l'​information dans l'​espace et pour me familiariser avec les assistants de preuve, afin d'​établir une garantie de correction pour l'​algorithme utilisé.
 +Puis j'ai étendu mes résultats de thèse au calcul parallèle utilisé dans la communauté HPC (High-Performance Computing), afin de capturer des paradigmes de communication entre processeurs.
 +
 +
 ====== Lambda-calcul ====== ====== Lambda-calcul ======
 +
 +J'ai été formé au lambda-calcul au master Logique Mathématique et Fondements de l'​Informatique de l'​Université Paris-Diderot.
 +Mon stage de M2 avec le professeur émérite Jean-Louis Krivine porta sur une extension de la correspondance preuve/​programme à la logique classique, en ajoutant des commandes comme callcc au lambda-calcul.
 +Cette approche m'​intéressa particulièrement car elle permet de donner un sens calculatoire aux théorèmes prouvés par les mathématiciens.
 +
 +J'ai travaillé durant la première partie de ma thèse avec le professeur Tristan Crolard sur une traduction dans le système T des commandes de continuation comme callcc} manipulant les contextes pour forcer syntaxiquement les stratégies d'​évaluation des programmes.
 +En m'​inspirant des travaux de Serge Grigorieff et Pierre Valarcher et des machines de Krivine, j'ai construit une représentation des stratégies contextuelles (par nom, par valeur et par besoin) du lambda-calcul sous forme d'​Abstract State Machine (ASM).
 +
  
 ===== Réalisabilité classique ===== ===== Réalisabilité classique =====
Ligne 47: Ligne 61:
  
 Voici {{ :​fr:​research:​lema.pdf |la dernière version}}. Voici {{ :​fr:​research:​lema.pdf |la dernière version}}.
 +
 +====== Algorithmes séquentiels ======
  
  
-====== Thèse ======+====== Thèse ​(TODO maj) ======