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.

• README
• HOL Light source
  
  

Publications

1. S. Khan-Afshar, O. Hasan and S. Tahar: Formal Analysis of Electromagnetic Optics [Novel Optical Systems Design and Optimization XVII (SPIE'14)]
   
   
2. 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.]
   
   
3. 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]
   
   
4. 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.
   
   
5. 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.
   
   
6. S. Khan-Afshar, O. Hasan, and S. Tahar. Formalization of Fabry Perot Resonator in HOL light. Technical Report, Concordia University, Montreal, Canada, 2013
   
   
7. 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.]