Abstract

Quantum optics plays an important role in many disciplines, such as quantum computers and quantum communication. Quantum optical system models and analysis, however, are very complex. Currently used analysis and verification techniques pose problems of safety, cost, soundness and completeness. In this paper, we propose to use HOL Light for the formalization and verification of quantum optics models. The proposed method consists of three layers that form the fundamentals of quantum optics: 1) Linear algebra aspects, 2) Quantum mechanics, and 3) Electromagnetic field quantization. We also provide components library that contains the definitions of the basic and commonly used quantum optical devices. As an application, we present the formal specification of quantum beam splitters and prove in HOL Light relevant properties, such as reversibility and energy preservation.

HOL Light Script

Core Formalization

• Layer One: Linear Algebra Aspects
• Layer Two: Quantum Mechanics
• Layer Three: Quantum Optics
• Utilities ( HOL-Light helper functions)

Applications

Beam Splitter

Description is given in the papers
• Quantum Devices