|
|
 |
|
Mardi 11 Février
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Petit voyage autour des sémantiques quantitatives de la logique linéaire |
| Description: |
Michele Pagani Une sémantique dénotationelle interprète les types de données (commeBool ou Int) par des espaces mathématiques (posets, treillis,structures algébriques) et les programmes par des fonctions sur cesespaces. L'intérêt d'une telle interprétation étant de donner unedescription du comportement opérationnel des programmes qui faitabstraction du langage dans lequel les programmes sont écrits.Les sémantiques quantitatives sont en particulier les sémantiquesdénotationelles issues de la logique linéaire, où les types de donnéessont interprétés par des espaces vectoriels (ou, plus généralement,des modules), les programmes qui utilisent exactement une fois leursdonnées d'entrée deviennent des fonctions linéaires (au sensalgébrique), alors que les programmes qui utilisent leurs ressourcesun nombre indéterminé de fois (comme les programmes récursifs ou lesprogrammes utilisant l'instruction while, par exemple) sontinterprétés par des fonctions analytiques, approximables par despolynômes, qui représentent des calculs partiels.Ces sémantiques sont particulièrement naturels pour décrire desprogrammes non-déterministes, voire probabilistes ou quantiques,l'addition exprimant une sorte de superposition des états élémentaireset les scalaires associant une estimation quantitative à une tellesuperposition.Dans cet exposé, je chercherai à donner une intuition del'interprétation des programmes via quelques exemples de sémantiquesquantitatives et à donner un aperçu des résultats récemmentobtenus, en particulier dans le cadre des langages fonctionnelsprobabilistes. |
|
|
