Q# as a Quantum Algorithmic Language

Abstract

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 $\lambda$-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 $\lambda$-Q#'s type system and present its equational semantics based on a fully complete algebraic theory by Staton.

In Proceedings QPL 2022, arXiv:2311.08375

References in corpus (5)

• Linear usage of state
• Formal Metatheory of Second-Order Abstract Syntax
• Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra
• Quantum Hoare Type Theory: Extended Abstract
• A HoTT Quantum Equational Theory (Extended Version)

Cited by in corpus (2)

• Networked Quantum Services
• Automated Verification of Silq Quantum Programs using SMT Solvers