Q# as a Quantum Algorithmic Language (The Essence of Q#)


Q# is a standalone domain-specific programming language from Microsoft for writing and running quantum programs. Like most industrial languages, it was designed without a formal specification, which can naturally lead to ambiguity in its interpretation. We aim to provide a formal language definition for Q#, placing the language on a solid mathematical foundation and enabling further evolution of its design and type system. This paper presents λ-Q#, an idealized version of Q# that illustrates how we may view Q# as a quantum Algol (algorithmic language). We show the safety properties enforced by λ-Q#’s type system and present its equational semantics based on a fully complete algebraic theory by Staton. This is the first part of the larger project defining the essence of Q#.

Sep 28, 2022 8:00 PM — 9:00 PM
Invited Talk at Mingsheng Ying’s research group

Bio: Kartik Singhal (https://ks.cs.uchicago.edu) is a PhD candidate at University of Chicago with a focus on the design and semantics of quantum programming languages. He started and maintains the Quantum Programming Languages & Verification Bibliography at https://git.io/qpl-bib which is a community resource aimed at providing canonical bibliographic entries in BibTeX and BibLaTeX formats.

Note: The talk video also includes a demo of the Quantum Programming Languages & Verification Bibliography on Mingsheng’s suggestion.