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.

Quantum Game of Life

Remember Conway's game of life? Here's a quantum version by Arrighi and Grattage that I came across on arXiv today. Abstract:

This research describes a three dimensional quantum cellularautomaton (QCA) which can simulate all other 3D QCA. This intrinsically universal QCA belongs to the simplest subclass of QCA: Partitioned QCA (PQCA). PQCA are QCA of a particular form, where incoming information is scattered by a xed unitary U before being redistributed and rescattered. Our construction is minimal amongst PQCA, having block size 2x2x2 and cell dimension 2. Signals, wires and gates emerge in an elegant fashion.

Quantum Computing for Molecular Energy Simulations

Another one from arXiv: Quantum Computing for Molecular Energy Simulations by Whitfield, Biamonte, and Aspuru-Guzik. Another way quantum computers can be put to use besides the often cited factoring.

The abstract:

Over the last century, a large number of physical and mathematical developments paired with rapidly advancing technology have allowed the field of quantum chemistry to advance dramatically. However, the lack of computationally efficient methods for the exact simulation of quantum systems on classical computers presents a limitation of current computational approaches. We report, in detail, how a set of pre-computed molecular integrals can be used to explicitly create a quantum circuit, i.e. a sequence of elementary quantum operations, that, when run on a quantum computer, to obtain the energy of a molecular system with fixed nuclear geometry using the quantum phase estimation algorithm. We extend several known results related to this idea and discuss the adiabatic state preparation procedure for preparing the input states used in the algorithm. With current and near future quantum devices in mind, we provide a complete example using the hydrogen molecule, of how a chemical Hamiltonian can be simulated using a quantum computer.