On the contrary to classical optical theories, quantum optics considers light as a stream of particles called photons. This concept reveals new properties and phenomena about light, especially at a low number of photons. The computer simulation of quantum systems is not practical since it is proved that quantum systems cannot be efficiently simulated on ordinary computers. We propose to use HOL Light for the formalization and verification of quantum optics models. Having such a formalization would allow the verification of quantum optical devices such as single-photon sources, photon-detectors, and optical amplifiers. Moreover, it will be very helpful in the analysis of quantum optical networks and quantum computers, which are a very promising alternative to classical computers. The figure below shows the formalization flow and the progress achieved. The project goes through three major steps: 1) Linear algebra aspects, 2) Quantum mechanics, and 3) Electromagnetic field quantization. We also provide a component library that contains the definitions of the basic and commonly used quantum optical devices.

HOL Code Scripts

We have formalized some fundamentals of quantum optics and also applied our work to formally verify that beam splitters preserve energy.

• README
• HOL Light source
  
  

References

[1] M. Yousri Mahmoud, S. Tahar: On the Quantum Formalization of Coherent Light in HOL, NASA Formal Methods Symposium (NFM'14), (To appear).

[2] M.Y. Mahmoud, V. Aravantinos, and S. Tahar: Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 413-427.]

[3] M.Y. Mahmoud, V. Aravantinos and S. Tahar: Towards the Formal Verification of Quantum Optical Systems [Proc. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS.12), Kyoto, Japan, November 2012, pp. 147-151.]