Schématiquement, un algorithme quantique est la description d'une suite d'opérations élémentaires à appliquer sur une mémoire composée de bits quantiques. Cette mémoire possède des propriètés bien particulières :
un bit quantique est non-duplicable ;
les opérations de modifications de la mémoire sont réversibles ;
les opérations de lecture sont probabilistes et modifient l'état global de la mémoire.
Les opérations réversible sont regroupées dans un "circuit quantique", version quantique du circuit booléen. Comme les bits quantiques ne sont pas duplicable, un circuit quantique est composé de fils parallèles, et chaque opération élémentaire travaille sur le même nombre de fils d'entrée que de fils de sortie.
Quipper est un langage fonctionel de description de circuits. Présentement implémenté comme sous-langage de Haskell, il permet la manipulation de bits quantiques, de listes de bits quantiques, mais aussi des circuits générés, pour par exemple les inverser, les répéter... Un exemple de circuit généré est comme suit:
Dans ce circuit, les entrées et sorties sont numérotées en vert. On voit bien que tous les fils sont complètement parallèles. On trouve sinon des initialisations de fils, et des désallocations avec assertions de valeur (les zeros en noir). On trouve aussi des portes Hadamard ("H"). Finalement, de nombreuse boite sont en fait des sous-circuits: les portes "OC" et les carrés noirs non-nommés.
De nombreuses questions sont ouvertes pour analyser les circuits générés par un programme donné:
Spécification et certification de la taille des circuits en fonction des paramètres du programme.
Contraintes sur certaines constructions. Par exemple, une primitive d'inversion de circuits ne peut qu'inverser un circuit réversible. Ou encore: un bit quantique n'est pas duplicable.
Assertion de valeur avant la désallocation de fil: dans certain cas, il est possible de vérifier l'assertion de façon statique.
Validation de la "forme" d'un circuit: si une sous-routine génère un circuit, est-ce le bon?
Certains problèmes sont solubles avec un système de type. D'autres ne le sont pas, mais sont potentiellement solubles avec un système d'assertion de code, ou de pré- et post-conditions.
Le stage porte sur le développement d'un outil de spécification et de certification des programmes écrits avec Quipper. Suivant l'intérêt de la personne choisie, on pourra se focaliser sur une ou plusieurs des problématiques proposées.
L'outil envisagé pour le développement est Wh3, une platforme pour la vérification de programme. Why3 propose un langage ML puissant (WhyML) et un langage de spécification: le but du stage sera de trouver comment encoder un programme Quipper en WhyML et de développer une librairie adaptée à la caractérisation de propriètés intéressantes.
Plusieurs algorithmes non-triviaux ont été implémentés dans le langage Quipper. Ces algorithmes serviront de base de travail pour tester l'outil développé.
Pour les besoins du stage, une connaissance du calcul quantique est complêtement optionnelle. Par contre, l'étudiant devra avoir une bonne connaissance de la programmation fonctionnelle. Une connaissance de Haskell serait un plus.
Encadrant : Benoit Valiron <benoit.valiron@lri.fr>.
Lieu du stage : Laboratoire de Recherche en Informatique (LRI), Univ. Saclay.