论文标题
Q＃作为量子算法语言
Q# as a Quantum Algorithmic Language
论文作者
论文摘要
Q＃是Microsoft的独立域特定编程语言，用于编写和运行量子程序。像大多数工业语言一样，它的设计没有正式规格，这自然会导致其解释中的歧义。我们旨在为Q＃提供正式的语言定义，将语言放在坚实的数学基础上，并能够进一步发展其设计和类型系统。本文介绍了$λ$ -Q＃，这是Q＃的理想化版本，说明了我们如何将Q＃视为量子algol（算法语言）。我们显示了由$λ$ -Q＃的类型系统强制执行的安全性能，并根据Staton的完全完整的代数理论介绍其方程式语义。
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.
