Soutenance : Conception d’un outil de formalisation des mathématiques basé sur le système formel W

Loading Map....

Date/Time
Date(s) - 15/06/2016
All Day

Location
ISCPIF

Categories


Conception d’un outil de formalisation des mathématiques basé sur le système formel W
& Détermination du nombre de codes circulaires de trinucléotides.

Par Matthieu Hermann, sous la direction de Alain Prouté
La soutenance aura lieu le 15 juin à 14h30 en salle 1.1 de l’ISC (113 rue Nationale) et sera suivi d’un pot.
Pour entrer dans l’institut: premier code, boîtier de gauche: 2709. Second code, boîtier de gauche: 2710.
La présentation, en français, portera sur la première partie des travaux de M. Herrmann dont voici le résumé:
« Le système formel W est une modélisation théorique des mathématiques. Dans cette thèse, nous étudions comment W peut servir de base à la réalisation d’un langage de programmation «en mathématiques», où les ensembles prennent la place habituellement dévolue aux types. Nous commençons par caractériser les connecteurs logiques par adjonctions, apportant un éclairage nouveau sur la conjonction dépendante et l’implication dépendante, ce qui nous permettra de définir formellement les quantifications dans les ensembles. Puis, nous définissons un nouveau système formel WBar mieux adapté à la réalisation d’un langage de programmation, et nous prouvons formellement son équivalence à W. Enfin, la programmation «par ensemble» nécessite la vérification statique d’énoncés en plus de la vérification classique des types. Pour cela, nous présentons un premier algorithme non seulement capable de prouver (dans une certaine mesure) un énoncé, mais aussi d’exhiber la preuve correspondante.»