GEORG STRUTH
dates de séjour
discipline
Fonction d’origine
Institution d’origine
pays d'origine
lien internet
projet de recherche
Cohérence algébrique, algèbres de Kleene de dimension supérieure et preuves interactives
Développées initialement pour modeler des systèmes informatiques, les algèbres de Kleene ont été généralisées récemment pour décrire des systèmes de réécriture de dimension supérieure en mathématiques. Ce projet vise à développer de nouvelles variantes de ces algèbres pour vérifier des propriétés de cohérence en algèbre catégorique. Pour cela il semble essentiel de formaliser cette approche avec des assistants de preuve pour apprivoiser la complexité des preuves dans les catégories supérieures. Le projet souligne particulièrement l’usage de ces algèbres dans le cadre des méthodes géométriques pour les systèmes informatiques concurrents et distribués. Du point de vu opérationnel, les algèbres visent à fournir une couche d’abstraction soutenant des preuves équationnelles avec des diagrammes catégoriques, des stratégies de réduction, et ainsi des preuves automatisées et un traitement algorithmique.
Les résultats envisagés seront par conséquent des nouvelles algèbres de Kleene de dimension supérieure (globulaires, (pré)cubiques et simpliciales), des preuves de cohérence pour les algèbres de dimension supérieure, la formalisation de l’approche avec un assistant de preuve de type Coq ou Isabelle, et son usage dans la concurrence, notamment avec des automates de dimension supérieure.
biographie
Georg Struth est professeur en informatique théorique à l’Université de Sheffield, Royaume Uni, et directeur de son laboratoire de vérification. Il a une longue expèrience en recherche sur les algèbres et logiques de programmes, leurs sémantiques, les méthodes de vérification et la formalisation des théories mathématiques avec des assistants de preuve.
Il est surtout connu pour son travail pionnier sur la théorie et les applications des algèbres de Kleene et des quantales, développant des variantes modales, variantes cylindriques, questions relatives à l'exhaustivité et à la décidabilité dans l'application aux programmes et la conception d'outils de vérification.
Son travail plus récent porte sur la vérification quantitative, la sémantique des systèmes probabilistes et hybrides (systèmes dynamiques interagissant avec des systèmes de contrôle discrets), les modèles géométriques de concurrence et de distribution utilisant la réécriture de dimension supérieure des polygraphes et les automates de dimension supérieure.
