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
fr:research:fssp [2017/03/20 14:25]
apeiron
— (Version actuelle)
Ligne 1: Ligne 1:
-[[https://​en.wikipedia.org/​wiki/​Firing_squad_synchronization_problem|Firing Squad Synchronization Problem]] 
  
-Depuis fin 2015 je fais un postdoc((Financé par l'ANR TARMAC 12 BS02 007 01.)) avec Jean-Baptiste Yunès et Luidnel Maignan à l'​Université Paris-Diderot sur le problème de la synchronisation dans les automates cellulaires. Je veux prouver que leur approche basée sur la modularité et des champs récursifs produit bien le résultat attendu, puis implémenter cette approche en utilisant l'​assistant de preuve Coq. 
- 
-L'​intérêt est double pour mon projet de recherche. D'une part, mon travail précédent s'est fait essentiellement sur la complexité en temps et la taille des éléments, alors que nous examinons aujourd'​hui les problèmes de voisinage et de transmission de l'​information dans l'​espace. D'​autre part, il s'est avéré que mon style de preuve << mécanique >> est idéal pour travailler avec un assistant de preuve, qui répond à mon intérêt pour la constructivité et notamment la relation preuve/​programme,​ ainsi qu'à mon intérêt pour la quête des fondements cette fois vue dans un cadre computationnel et plus seulement logique. 
- 
-Le rapport technique est encore en rédaction, voici {{ :​fr:​research:​rapport11.pdf |la version actuelle}}