Mário Silva (Mocqua) will defend his thesis on Monday, July 7th at 2pm in room C005, with a presentation entitled Programming languages characterizing quantum efficiency.
Jury:
– Ugo Dal Lago (rapporteur), Università di Bologna
– Benoît Valiron (rapporteur), CentraleSupélec, Université Paris-Saclay, LMF
– Gilles Barthe (examinateur), MPI-SP Bochum, IMDEA Software Institute
– Cristina Sernadas (examinatrice), Instituto Superior Técnico, Universidade de Lisboa
– Romain Péchoux (directeur de thèse), Loria, Université de Lorraine
– Emmanuel Hainry (co-directeur de thèse), Loria, Université de Lorraine
Abstract:
Quantum computing is a paradigm of computation where quantum physical phenomena such as entanglement and superposition are used to obtain an advantage over classical computation. While the quantum programmer has a large choice of programming languages at their disposal, none allow for ensuring the feasibility of their programs. To this end, we introduce a first-order quantum programming language (FOQ) that allows for reasoning about the physical realizability and complexity of quantum programs.
We introduce statically-checked restrictions over FOQ program that allow us to identify fragments that are sound and complete for quantum polynomial (PFOQ) and polylogarithmic time (LFOQ). We provide a number of examples of polynomial and polylogarithmic time programs that are captured by these fragments, and constitute relevant quantum functions, such as the quantum Fourier transform, quantum arithmetic, and examples like binary search.
We also introduce new compilation techniques that allow for translating PFOQ and LFOQ programs into circuits of adequate complexity, avoiding the exponential blow-up that can occur from the recursive use of a quantum control statement. We further improve this compilation technique and are able to define a FOQ fragment that is sound and complete for quantum polynomial time where the circuit complexity of the quantum case statement is the maximum of the branches, instead of their sum. We develop a prototype compiler that implements these ideas over PFOQ and LFOQ programs.