Différences
Ci-dessous, les différences entre deux révisions de la page.
Les deux révisions précédentes 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 17:53] 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 ===== |