PhD Defence: Dongho Lee

Jul 21 14:00 ₂₀₂₂

Abstract: The quantum random-access machine (QRAM) model is a practical model of quantum computation composed of a classical computer and a quantum processor communicating with each other. The program is executed on the classical computer. It can send instructions corresponding to quantum operations and receive measurement outcomes from the quantum co-processor. This model is expected to be the model of quantum computation in the near future, and a group of quantum programming languages has been developed based on it.

While the program in the model has the ability to simulate any quantum circuit with the help of a quantum processor, analyzing the program becomes difficult without relying on another quantum computer. This problem calls for the development of formal methods for quantum programming languages: formal tools to develop and reason on code optimization, analyze resources, and specify and prove the properties of quantum programs.

One of these tools is categorical semantics, which links the actions of quantum operators to the meaning of quantum programs and embeds logical systems on quantum states to the type system of the language. Although categorical semantics for quantum programming languages is an established field, dynamic lifting ---the ability to use the result of a measurement in the classical host--- has so far only been considered in the context of denotational semantics based on operator algebras: a circuit in the model is not a syntactic object that can be manipulated.

In this thesis, we formalize dynamic lifting in a quantum circuit-description language which allows programs to transfer the result of measuring quantum data into classical data. Following the Proto-Quipper approach, we define a typed circuit-description language called Proto-Quipper-L, where the lifted data is encoded in the branching structure. Dynamic lifting is then formalized within the operational and categorical semantics.

Our categorical semantics is based on the model from Rios\&Selinger for Proto-Quipper-M. However, to formalize dynamic lifting, we construct, on top of a concrete category of circuits with measurements, a Kleisli category, capturing the measurement as a side effect. We show the soundness of this semantics with regard to the operational semantics.

Jury:

• Delia Kesner (President) : Professeure, IRIF, Université de Paris
• Ugo Dal Lago (Reviewer) : Professeur, Université de Bologne
• Lionel Vaux (Reviewer) : Maître de conférences, LdP, Université d’Aix-Marseille
• Chantal Keller (Examiner) : Maîtresse de conférences, LMF, Université Paris-Saclay
• Frédéric Boulanger (Director of thesis) : Professeur, CentraleSupelec, Université Paris-Saclay
• Benoît Valiron (Supervisor) : Professeur assistant, CentraleSupelec, Université Paris-Saclay
• Valentin Perrelle (Supervisor) : Ingénieur-Chercheur, CEA-LIST, Université Paris-Saclay