Kartik Singhal (University of Chicago) |
Kesha Hietala (University of Maryland) |
Sarah Marshall (Microsoft Quantum) |
Robert Rand (University of Chicago) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.394.10 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |