Le professeur du Département d’informatique Ryan Kavanagh a reçu une subvention de 25 000 $ du Conseil de recherches en sciences naturelles et en génie (CRSNG) dans le cadre du concours des Subventions Catalyseur en quantique du programme Alliance, volet international pour son projet intitulé «Fondements sûrs des langages de programmation classique et quantique». Cet octroi s’inscrit dans le cadre de la Stratégique quantique nationale du Canada. La cotitulaire du projet est la professeure Brigitte Pientka, de l’Université McGill. Les professeurs Peng Fu, de l’University of South Carolina, et Kohei Kishida, de l’University of Illinois at Urbana-Champaign, collaborent également à la recherche.
L’informatique quantique accélérera considérablement les secteurs dépendants de capacités de calcul massives, tels que la recherche pharmaceutique, la modélisation climatique et l’intelligence artificielle. Toutefois, les ordinateurs quantiques sont très coûteux à faire fonctionner. Cela implique que l’on ne peut pas compter sur la méthode traditionnelle d’exécution et de débogage de code et qu’on doit s’assurer que les programmes quantiques sont corrects avant de les lancer. Les langages de programmation sûrs garantissent l’absence de divers types de défaillances logicielles avant même que les programmes ne soient exécutés.
Le langage de programmation quantique Quipper a eu un très grand impact grâce à sa capacité d’implémenter des programmes quantiques très complexes. Malheureusement, des erreurs peuvent survenir dans des programmes Quipper au cours de l’exécution à cause d’interactions entre les fonctionnalités du langage. Les chercheurs travaillent depuis longtemps à assurer des propriétés de sûreté pour divers sous-ensembles des fonctionnalités de Quipper. Toutefois, ces fragments de langage sont souvent formulés à l’aide d’abstractions complexes et ad hoc qui varient selon le fragment.
Le projet subventionné consiste à reformuler l’essentiel de Quipper en termes d’abstractions standards, sûres, et fréquemment utilisées par les chercheurs qui étudient les fondements des langages de programmation. Cette reformulation offre une théorie unificatrice pour les différents fragments déjà étudiés et un fondement pour des recherches futures sur les langages quantiques.
Pour Ryan Kavanagh et sa collègue Brigitte Pientka, il s’agit d’une nouvelle collaboration avec les professeurs Peng Fu, de l’University of South Carolina, et Kohei Kishida, de l’University of Illinois, visant à concevoir un langage de programmation pour le calcul quantique-classique hybride. Les algorithmes hybrides entrelacent le calcul quantique et le calcul classique. En cours d’exécution, ils mesurent les circuits quantiques et utilisent ces résultats pour ajuster ou générer de nouveaux circuits exécutés ensuite par le coprocesseur quantique. Cette fonctionnalité est utilisée par des techniques de programmation quantiques telles que «retry-until-success» et les algorithmes de correction d’erreurs. Elle peut aussi réduire le nombre de qubits (bits quantiques) requis, ainsi que la profondeur et la taille des circuits quantiques.
Ces optimisations sont cruciales au regard des limitations des ordinateurs quantiques actuels. Le chercheur et ses collaborateurs proposent de valider la sûreté de leur langage en recourant à un assistant de preuve, soit un logiciel spécialisé pour la vérification de preuves formelles. Cela leur permettra d’obtenir des garanties de sûreté formelles et vérifiées pour leur langage et pour les programmes qu’il servira à écrire.