Overview
- Responsible professor: Dominique Unruh
- Supervisor: Benjamin Stutte
- Semester: Summer 2025
- Level: Bachelor / Master
About
When programming a quantum computer, one preferably does not want to manually come up with a list of operations that are applied to individual qubits. In the same way as one does not want to program classical computers by applying AND, OR, and NOT gates to individual bits. Because of that, there are a multitude of different programming languages for quantum computers, both applied ones, and languages with deeper theoretical foundations.
In this seminar, each participant will be studying one such program language from a scientific paper, and present the results to their peers in a talk and a seminar report.
Deadlines and Structure
All in-person meetings will take place in the seminar room for our chair. Route description.
Date | Event |
---|---|
TBD | Kick-off meeting |
TBD (3 Days) | Topic selection |
TBD (8 Weeks) | First-draft and peer-review assignments |
TBD (1 Week) | Peer-review submissions |
TBD (1 Week) | Paper submission |
TBD (2 Weeks) | Presentation slides submission |
TBD (~2 Weeks) | Seminar talks 1 |
TBD (1 Day) | Seminar talks 2 |
During the kick-off meeting, you will get a small introduction to each language. You then have three days to give two rankings for these languages: the first one indicates which language you would like to write your paper about and the second one, which language you would like to write a review for during the peer-review process. I will assign you a topic the next day. In the following two months, you will then work on a first draft for a paper where you describe the core features and use-cases of your language.
When the first drafts have been submitted, you will be sent the paper of an other student to write a review for. These peer-reviews have to be submitted a week later and after the review you have an additional week to work the feedback into your final paper.
After the deadline for the final paper, you have two weeks to prepare slides. Two weeks after the slide submissions, the talks will then be held on two successive days. The exact dates of these two meetings will be determined during the semester.
Submission requirements
- Paper: about 5-10 Pages
- Talk: 25 Minutes
Grading
The paper and your presentation contribute in equal parts to the final grade.
Languages
You can choose either an applied language or a theoretical one. Applied languages are ones that you can actually run and theoretical ones are purely formal.
Applied languages
Name | Description |
---|---|
SilQ | High-level language developed at ETH Zürich which aims to offer intuitive semantics and a strong static type system. Website, Article |
Quipper | Functional language embedded in Haskell. Website, Article |
OpenQASM | An assembly language to describe quantum circuits. Website, Article |
Q# | High-level language developed by Microsoft. Works in conjunction with C#, Python and F#. Website, Article |
Qiskit/Cirq/pyQuil | These are not necessarily stand-alone languages and moreso Python libraries that offer syntax for circuit design. If you are assigned this topic, you can write about any subset of these three these languages. Qiskit Website, Qiskit Article. Cirq Repository. pyQuil Repository |
Scaffold | High-Level C-Like language that compiles to QASM. Article, Repository of the Scaffold compiler |
Qmod | The high-level language used in the quantum IDE Classiq. Description on the Classiq website, Article |
Theoretical languages
Name | Description |
---|---|
Proto-Quipper | In the list above, you can see the language Quipper, which is embedded in Haskell. Proto-Quipper is a project aimed at providing a formalization of Quipper that can be used as a testbed to develop reasoning techniques for quantum programming. Proto-Quipper-M provides the general framework and semantics. There are multiple extensions such as Proto-Quipper-D, which defines a dependent linear type system or Proto-Quipper-Dyn which defines dynamic lifting. |
QUIRE | Theoretical language for defining quantum circuits. Article. There is also a an implementation the proof assistant Rocq. |
Selinger’s Quantum Lambda Calculus | A quantum-extension of the lambda calculus 2005 Paper, 2009 Paper |
Selinger’s Quantum Flow Charts | Traditionally, quantum algorithms are expressed on the hardware level which does not encourage abstractions such as data types. Selinger proposes a language that can be represented in the form of flow-charts. Article |
Ying’s qGCL | The Guarded Command Language (GCL) is a formal language defined by Disjkstra to facilitate reasoning about program correctness. In “Foundations of Quantum Programming”, Mingsheng Ying defines a quantum extenson of it. |
Prerequisites
You should have taken an introductory course related to quantum computing or quantum algorithms. (E.g., Introduction to Quantum Computing)