Abstract

During the last decade, formal methods, in particular theorem proving, have proven to be effective as analysis tools in different fields. Among them, quantum optics is a potential area of the application of theorem proving that can enhance the analysis results of traditional techniques, e.g., paper-and-pencil and lab simulation. In this paper, we present the formal definition of coherent light, which is typically a light produced by laser sources, using higher-order logic and show the effect of quantum operations on it. To this aim, we first present the formalization of underlying mathematics, in particular, finite/infinite summation over quantum states, then prove important theorems, such as uniqueness and the effect of linear operators. Thereafter, basic quantum states of light, called fock states, are formalized and many theorems are proved over such states, e.g., the effect of the quantum creation operation over fock states. Finally, the fundamental notions of coherent light are formalized and their properties also verified.

HOL Light Script

Utilities

• Follow steps in the Utilities

Core Formalization

• Quntum States Space
• Infinite Summation
• Quantum States and Operators
• Single mode
• Coherent States