A Framework for Formal Reasoning about Geometrical Optics

Recently, optics technology has emerged as a promising solution by resolving critical bottlenecks in conventional electronic systems. Its application domain spans over diverse fields ranging from laser surgeries to space telescopes. In this paper, we describe an ongoing project which aims at building a theorem proving based framework for the formal reasoning about geometrical optics, an essential theory required in the design and analysis of optical systems. Mainly, we present the motivation of our work, a road-map to achieve our goals, current status of the project and future milestones.