Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a complete program and only then verifies its correctness. In this work, we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose a set of refinement rules to construct correct programs in a quantum while language. We validate QbC by constructing quantum programs for two idiomatic problems, teleportation and search, from their specification. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play an important role in supporting the design and taxonomization of quantum algorithms and software.

A future quantum network will allow distributing entanglement over in principle arbitrarily long distances. This topic holds importance for applications in quantum information science as well as for fundamental investigations and currently receives significant attention around the world. The most promising approach for achieving long-distance quantum communication is to use quantum repeaters, many of which employ optical quantum memories to store quantum information. Among the candidates for building such quantum memories, rare earth ion-doped crystals exhibit noteworthy promise.  In this context, our research delves into the exploration of a thulium-doped yttrium gallium garnet crystal (Tm: YGG) at ultralow temperatures, as low as 500 mK. This crystal offers an optical coherence time exceeding one millisecond and a ground-state Zeeman-level lifetime as long as tens of seconds. We take advantage of such exceptional features to show a series of pivotal experiments. These include the storage of optical pulses for durations of up to 100 μs, frequency-multiplexed storage of multiple frequency modes, and a proof-of-principle demonstration showcasing the selective retrieval of stored frequency modes.  Furthermore, I will also shed some light on the optical coherence and relaxation dynamics of Tm: YGG, which is crucial for the development of an efficient quantum memory. Our results suggest that Tm: YGG exhibits substantial potential as a multimode optical quantum memory within the framework of a frequency-multiplexed quantum repeater architecture. 

We explore the interplay between symmetry and randomness in quantum information. Adopting a geometric approach, we consider states as H-equivalent if related by a symmetry transformation characterized by the group H. We then introduce the Haar measure on the homogeneous space U/H, characterizing true randomness for H-equivalent systems. While this mathematical machinery is well-studied by mathematicians, it has seen limited application in quantum information: we believe our work to be the first instance of utilizing homogeneous spaces to characterize symmetry in quantum information. This is followed by a discussion of approximations of true randomness, commencing with t-wise independent approximations and defining t-designs on U/H and H-equivalent states. Transitioning further, we explore pseudorandomness, defining pseudorandom unitaries and states within homogeneous spaces. Finally, as a practical demonstration of our findings, we study the expressibility of quantum machine learning ansatze in homogeneous spaces. Our work provides a fresh perspective on the relationship between randomness and symmetry in the quantum world.

Introduced in 2010 by Scott Aaronson and Alex Arkhipov, Boson sampling is a specific quantum task demonstrating that a quantum device, even in the presence of noise, can outperform classical computers. In this presentation, I will introduce the Boson sampling problem and its implementation using neutral atoms instead of photons. Additionally, I will discuss an extension of this work involving on-site interactions, specifically the Bose-Hubbard model. Furthermore, I will touch upon the unexpected real-world application of boson sampling in seemingly unrelated blockchain networks. If time allows, I will also cover my work on quantum algorithms for thermal state preparation using fluctuation theorems.

Optical photons are excellent quantum information carriers, but weak optical nonlinearity poses significant challenges to these systems' scalability and computational capabilities. Currently, only probabilistic methods can achieve nonlinear quantum operations crucial for universality and fault tolerance, restricting the clock speed and making it challenging to scale due to significant resource overhead. Ultrafast quantum nanophotonics with second-order optical nonlinearity presents a potential solution to overcome these challenges. In this talk, we will discuss recent experimental advances, including the on-chip generation and measurement of ultra-broadband squeezed states and all-optical realizations of switching and nonlinear functions in an emergent thin-film lithium niobate platform. We further delve into how enhanced optical nonlinearity can enable novel functionalities such as photon-number-resolving measurements and deterministic quantum state engineering, offering a practical path to scalable, fault-tolerant quantum information processors at room temperature.