Light, as an electromagnetic wave phenomenon, is described by the
same theoretical principles that govern all forms of electromagnetic
radiation.
We employ theorem proving as a complement to computational
and numerical approaches to improve optical model analysis
in a formal analysis framework. We provide the formalization of fundamental
physical theories and laws to reason about the behaviour of light
as electromagnetic waves in higher-order logic to verify its key properties
using the HOL Light theorem prover.
We also plan to formalize necessary mathematical background to model an optical device based on electromagnetic theory.

## HOL Scripts

We have formalized some fundamentals of Electromagnetic optics.

## Publications

- S. Khan-Afshar, O. Hasan and S. Tahar:
Formal Analysis of Electromagnetic Optics [Novel Optical Systems Design and Optimization XVII (SPIE'14)]

- S. Khan-Afshar, O. Hasan and S. Tahar:
Towards the Formal Verification of Optical Interconnects
[Proc. IEEE New Circuits and Systems Conference (NEWCAS'14), Trois-RiviÃ¨res, Quebec, Canada, June 2014, pp. 157-160.]

- S. Khan-Afshar, V. Aravantinos, O. Hasan and S. Tahar:
Formalization of Complex Vectors in Higher-Order Logic [In: S. Watt, J. Davenport, A. Sexton, P. Sojka and
J. Urban (Eds.), Intelligent Computer Mathematics (CICM'14), Lecture Notes in Computer Science 8543, Springer, pp. 123-127]

- S. Khan-Afshar, U. Siddique, M. Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan,
and S. Tahar:
Formal Analysis of Optical Systems Mathematics in Computer Science, Vol. 8, No. 1, Springer, May 2014, pp. 39-70.

- S. Khan-Afshar, V. Aravantinos, O. Hasan, and S. Tahar.
A toolbox
for complex linear algebra in HOL Light. Technical Report, Concordia
University, Montreal, Canada, 2014.

- S. Khan-Afshar, O. Hasan, and S. Tahar. Formalization of Fabry
Perot Resonator in HOL light. Technical Report, Concordia University,
Montreal, Canada, 2013

- O. Hasan, S. Khan-Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL S. Berghofer et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]