PhD Position F/M PhD Position / Quantum programming with (co)inductive types.
Team: Mocqua, INRIA Nancy Grand-Est, mocqua.loria.fr
The PhD thesis will be jointly supervised by Romain Péchoux (Associate Professor, HDR, Université de Lorraine, email@example.com) and Vladimir Zamdzhiev (ISFP, Inria, firstname.lastname@example.org).
This PhD position is subject to be funded by Inria cordi-S programme.
Quantum technologies have led to the emergence of a new promising computational paradigm which can efficiently solve problems considered to be intractable on classical computers. Recent developments highlight the necessity of filling the gap between quantum algorithms and the actual quantum computers on which they have to be executed.
As a consequence, quantum programming languages play a key role in the future development of quantum computing. However, most existing quantum languages are fairly low-level: all of the quantum phenomena which induce computational speedup (compared to classical computation) are restricted to quantum bits, also known as qubits, and the operations which allow us to modify qubits are low-level quantum gates. This low-level machinery, comparable to boolean circuits, requires the programmer to focus on cumbersome architectural details, rather than focusing on algorithmic and high-level patterns. Because of this, there is a strong need to develop high-level quantum programming languages, where phenomena, such as superposition and entanglement, are available at higher quantum types, not just qubits.
Towards this direction, quantum types generalizing standard classical ones have to be introduced and corresponding type systems and programming languages for manipulating them have to be studied. These types can be inductively defined, e.g., quantum natural numbers and quantum lists, hence allowing us to form superpositions and entanglement patterns of nats, lists, etc., and not just qubits. Alternatively, they can be coinductively defined, e.g., infinite streams of qubits, which poses difficult research questions for quantum programming language design, due to the infinitary nature of this data. Designing a suitable formalism to solve these issues would have an impact on quantum programming languages and would enable programmers to write high-level and more concise code.
This PhD project aims at studying substructural and quantum type systems with inductive and coinductive types. The applicant will design and study the type-theoretic, operational and denotational aspects of the corresponding languages and systems.
Towards that end, particular attention will be paid to the following tasks:
- Design a quantum programming language with (co)inductive types and a type-safe operational semantics, where superposition and entanglement are first-class resources available at all types, not just qubits.
- Define a suitable denotational (i.e., mathematical) semantics of this language and demonstrate its soundness and adequacy with respect to the operational semantics.
- Study important behavioral properties of this language, such as productivity and complexity.
 P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14:4, 2004.
 P. Selinger, B. Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16:3, 2006.
 R. Péchoux, S. Perdrix, M. Rennela, V. Zamdzhiev. Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. FoSSaCS 2020.
 B. Lindenhovius, M. W. Mislove, V. Zamdzhiev. Mixed linear and non-linear recursive types. ICFP 2019.
 R. Clouston, A. Bizjak, H. B. Grathwohl, L. Birkedal. Programming and Reasoning with Guarded Recursion for Coinductive Types. FoSSaCS 2015.
 R. Atkey, C. McBride. Productive coprogramming with guarded recursion. ICFP 2013.
 R. Péchoux. Implicit Computational Complexity: Past and Future. Habilitation thesis. Université de Lorraine, 2020.
 M. Avanzini, G. Moser, R. Péchoux, S. Perdrix, V. Zamdzhiev. Quantum Expectation Transformers for Cost Analysis, 2022.
Master's degree, or equivalent, in theoretical computer science or mathematics;
Language and Skills
Ability to work independently as well as in a team; Good skills in English; Optional: Knowledge of type systems and/or logic; Optional: Knowledge of quantum computation.
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
Salary: 1982€ gross/month for 1st and 2nd year. 2085€ gross/month for 3rd year.
Monthly salary after taxes : around 1596,05€ for 1st and 2nd year. 1678,99€ for 3rd year.
- Theme/Domain : Security and Confidentiality
- Town/city : Villers lès Nancy
- Inria Center : CRI Nancy - Grand Est
- Starting date : 2022-09-01
- Duration of contract : 3 years
- Deadline to apply : 2022-05-02