Green: Towards a formally verified functional quantum programming language

I saw this posted the other day, a PhD thesis by Green out of University of Nottingham: Towards a formally verified functional quantum programming language. This is another Haskell approach. As I said in my dissertation, I think there are serious obstacles in using a functional approach to quantum programming in a commercial development environment. Nonetheless it is good to see another quantum programming approach put out there. Here's the abstract:

This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally verified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the “Quantum IO Monad”, this framework is designed following a structural approach as given by a categorical model of quantum computation.

D'Hondt and Vandriessche: Distributed Quantum Programming

D'Hondt and Vandriessche have posted a paper on arXiv titled Distributed Quantum Programming. The technique the paper describes is pretty mathematical, so I wouldn't classify it as a "practical" approach to quantum programming. Nonetheless, it is great to see continued work in the subject. At the end of the paper they discuss a "distributed quantum virtual machine", which is also worth checking out. Good to see details of how we may actually interact with quantum computers in standard way- taking Knill's QRAM a step farther. They also describe a GUI for the quantum virtual machine's design tool:

(Image is from the paper itself.)

Here's the abstract of the paper:

In this paper we explore the structure and applicability of the Distributed Measurement Calculus (DMC), an assembly language for distributed measurement-based quantum computations. We describe the formal language’s syntax and semantics, both operational and denotational, and state several properties that are crucial to the practical usability of our language, such as equivalence of our semantics, as well as compositionality and context-freeness of DMC programs. We show how to put these properties to use by constructing a composite program that implements distributed controlled operations, in the knowledge that the semantics of this program does not change under the various composition operations. Our formal model is the basis of a quantum virtual machine construction for distributed quantum computations, which we elaborate upon in the latter part of this work. This virtual machine embodies the formal semantics of DMC such that programming execution no longer needs to be analysed by hand. Far from a literal translation, it requires a substantial concretisation of the formal model at the level of data structures, naming conventions and abstraction mechanisms. At the same time we provide automatisation techniques for program specification where possible to obtain an expressive and user-friendly programming environment.

NIST Creates a 2 Qubit Programmable Quantum Computer

At the National Institute of Standards and Technology (NIST) they've done it again: they've created a 2 qubit programmable quantum computer. The key word here is programmable, it can carry out an arbitrary sequence of operations. We still need to scale things up, but this is another important milestone.

(NIST Post doc David Hanneke doing a demo of the quantum computer. Image from NIST.)

Cove Presentation Posted

I did a presentation on Cove (the quantum computer programming framework I've developed) last week at Colorado Technical University. It is the slides that are in the last post, along with my presentation of them and some question and answers.