Outils

Agenda de l'ENS de Lyon

Sémantique des Jeux Quantique

Date
lun 28 sep 2020
Horaires

14H00

Lieu(x)
Intervenant(s)

Soutenance de Marc de Visme sous la Direction de Olivier Laurent et la Co-direction de M. Glynn WINSKEL

Organisateur(s)
Langue(s) des interventions
Description générale

Cette thèse porte sur la sémantique des langages de programmation quantiques, et en particulier sur celle du lambda-calcul quantique, un langage paradigmatique dû à Selinger et Valiron qui marrie flot de contrôle classique riche (fonctions d’ordre supérieur, récursion, etc) avec des données quantiques (création de qubits, mesure, application d’opérateurs unitaires). Pour donner un modèle du lambda-calcul quantique, il convient de trouver une alliance harmonieuse entre les modèles traditionnels de sémantique dénotationnelle (qui donnent du sens aux programmes en les interprétant dans des univers mathématiques adéquats) et les mathématiques du quantique (espaces de Hilbert, matrices de densité, etc).

Cette thèse comporte trois contributions principales :

Premièrement, nous étendons la sémantique des jeux, une approche dynamique à la sémantique dénotationnelle, au cas quantique. Nous obtenons le premier modèle dénotationnel du lambda-calcul quantique complet qui soit à la fois compositionnel et interactif, c’est à dire qu’il représente la dynamique de l’exécution. Notre modèle est une généralisation naturelle de développements récents pour le cas probabiliste.

Deuxièmement, nous relions formellement notre modèle au principal modèle dénotationnel pré-existant du lambda-calcul quantique complet, le modèle relationnel quantique dû à Pagani, Selinger et Valiron.

Finalement, nous montrons que notre modèle de jeux est pleinement adéquat, la correspondance idéale entre un langage de programmation et sa sémantique dénotationnelle. Nous en déduisons que le modèle relationnel quantique était lui-aussi pleinement adéquat, un problème que ses auteurs avaient laissé ouvert.

Gratuit

Mots clés

Disciplines