Showing 1–5 of 5 results for author: Singhal, K

Q# as a Quantum Algorithmic Language

Authors: Kartik Singhal, Kesha Hietala, Sarah Marshall, Robert Rand

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 i… ▽ More 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. △ Less

Submitted 15 November, 2023; v1 submitted 7 June, 2022; originally announced June 2022.

Comments: In Proceedings QPL 2022, arXiv:2311.08375

Journal ref: EPTCS 394, 2023, pp. 170-191

Quantum Hoare Type Theory: Extended Abstract

Authors: Kartik Singhal, John Reppy

Abstract: As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose… ▽ More As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs from being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress. △ Less

Submitted 5 September, 2021; originally announced September 2021.

Comments: In Proceedings QPL 2020, arXiv:2109.01534. See expanded version at arXiv:2012.02154

ACM Class: F.3.1; D.1.1; D.2.4; D.3.1; F.4.1

Journal ref: EPTCS 340, 2021, pp. 291-302

Gottesman Types for Quantum Programs

Authors: Robert Rand, Aarthi Sundaram, Kartik Singhal, Brad Lackey

Abstract: The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set H, S and CNOT. The Gottesman-Knill theorem showed that we can use this representation to efficiently simulate Clifford circuits. We show that Gottesman's semantics for quantum programs can be treated as a type syst… ▽ More The Heisenberg representation of quantum operators provides a powerful technique for reasoning about quantum circuits, albeit those restricted to the common (non-universal) Clifford set H, S and CNOT. The Gottesman-Knill theorem showed that we can use this representation to efficiently simulate Clifford circuits. We show that Gottesman's semantics for quantum programs can be treated as a type system, allowing us to efficiently characterize a common subset of quantum programs. We also show that it can be extended beyond the Clifford set to partially characterize a broad range of programs. We apply these types to reason about separable states and the superdense coding algorithm. △ Less

Submitted 5 September, 2021; originally announced September 2021.

Comments: In Proceedings QPL 2020, arXiv:2109.01534. arXiv admin note: substantial text overlap with arXiv:2101.08939

ACM Class: F.3.1; D.2.4; F.4.1

Journal ref: EPTCS 340, 2021, pp. 279-290

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Authors: Aarthi Sundaram, Robert Rand, Kartik Singhal, Brad Lackey

Abstract: We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the tra… ▽ More We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate. △ Less

Submitted 19 March, 2025; v1 submitted 21 January, 2021; originally announced January 2021.

Comments: 52 pages, 3 figures

ACM Class: F.3.1; D.2.4; F.4.1; I.1.1

Quantum Hoare Type Theory

Authors: Kartik Singhal

Abstract: As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare… ▽ More As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. Inspired by Hoare Type Theory in classical computing, we propose Quantum Hoare Type Theory (QHTT), in which precise specifications about the modification to the quantum state can be provided within the type of computation. These specifications within a Hoare type are given in the form of Hoare-logic style pre- and postconditions following the propositions-as-types principle. The type-checking process verifies that the implementation conforms to the provided specification. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. △ Less

Submitted 15 November, 2021; v1 submitted 3 December, 2020; originally announced December 2020.

Comments: UChicago CS master's paper. 34 pages, 12 code listings. Preliminary version accepted at QPL'20: arXiv:2109.02198

ACM Class: F.3.1; D.1.1; D.2.4; D.3.1; F.4.1