Overview
- Responsible professor: Dominique Unruh
- Supervisor: Benjamin Stutte
- Semester: Summer 2026
- 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 of our chair. Route description.
Tentative timeline (subject to changes depending on availability of staff and students):
| Date | Event |
|---|---|
| TBD | Kick-off meeting |
| TBD (3 Days) | Topic preference deadline |
| TBD (8 Weeks) | Preprint submission |
| TBD (1 Week) | Peer-review submission |
| TBD (2 Weeks) | Presentation slides submission |
| TBD (~2 Weeks) | Seminar talks 1 |
| TBD (1 Day) | Seminar talks 2 |
| TBD (1 Week) | Paper submission |
Topic Selection and Preprint
During the kick-off meeting, you will get a small introduction to each language. You then give two rankings for these languages (topic preferences): 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. In the following two months, you will then work on a first draft (called the preprint) of a paper where you describe the core features and use-cases of your language.
Peer-Review
When the preprints have been submitted, you will be sent the paper of another student to write a review for.
Presentations and Final Paper
After the deadline for the peer-reviews, you have to submit slides and prepare a talk. The talks will be held on two consecutive days. They should be 25 minutes long and are followed by a 20-minute segment of questions. Afterwards, you have an additional week to work on your final paper.
Submission requirements
- Paper: about 15 Pages
- Talk: 25 Minutes
Grading
Submission of the preprint, review, presentation slides and the final paper are mandatory. The preprint, presentation slides and final paper are considered in your grade. Your final submission is expected to address the peer-review and ambiguities that were pointed out during the presentation (based on audience question). This will also be considered in the grading.
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 with automatic uncomputation for ancillas. Website, Article |
| Quipper | Functional language embedded in Haskell. Website, Article, Up-To-Date Fork |
| Qimaera | Functional language embedded in Idris. GitHub Repo, 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/Qmod | 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. Description of Qmod, Qmod Article |
| Quil | Instruction language for an abstract machine with existing compiler and Python library for code generation and simulation. Paper, Repository of the PyQuil library |
Theoretical languages
| Name | Description |
|---|---|
| Selinger’s Quantum Lambda Calculus | A quantum-extension of the lambda calculus 2005 Paper, 2009 Paper |
| Proto-Quipper | Project aimed at providing a formalization of Quipper that can be used as a testbed to develop reasoning techniques for quantum programming. Proto-Quipper-S (Chapter 8 of this thesis) is a variant of a quantum lambda calculus. Proto-Quipper-M provides a general framework with categorical semantics. There are multiple extensions such as Proto-Quipper-Dyn which defines dynamic lifting. There is also Proto-Quipper-D, which defines a dependent linear type system (but is not an extension of Proto-Quipper-M). |
| SQIR | Kesha Hiethala developed a verified optimizer for quantum ciruits (VOQC). Internally, it uses the SQIR language for circuit representation. The tools run with the Rocq proof assistant. Press-Release, Article, GitHub Repository |
| 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 |
| Lambda-Q# | Idealized subset of Q# to provide it with safety guarantees Paper. |
Prerequisites
You should have taken an introductory course related to quantum computing or quantum algorithms. (E.g., Introduction to Quantum Computing)