Formal analysis of optical systems

DOI10.1007/S11786-014-0175-ZzbMATH Open1302.68245arXiv1403.3039OpenAlexW2139371904MaRDI QIDQ475384FDOQ475384

Authors: Sanaz Khan-Afshar, Umair Siddique, Mohamed Yousri Mahmoud, Vincent Aravantinos, Ons Seddiki, Osman Hasan, Sofiène Tahar 

Publication date: 26 November 2014

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Abstract: Optical systems are becoming increasingly important by resolving many bottlenecks in today's communication, electronics, and biomedical systems. However, given the continuous nature of optics, the inability to efficiently analyze optical system models using traditional paper-and-pencil and computer simulation approaches sets limits especially in safety-critical applications. In order to overcome these limitations, we propose to employ higher-order-logic theorem proving as a complement to computational and numerical approaches to improve optical model analysis in a comprehensive framework. The proposed framework allows formal analysis of optical systems at four abstraction levels, i.e., ray, wave, electromagnetic, and quantum.

Full work available at URL: https://arxiv.org/abs/1403.3039

Recommendations

• On the formal analysis of Gaussian optical systems in HOL
• Formal Analysis of Optical Waveguides in HOL
• A Framework for Formal Reasoning about Geometrical Optics
• On the Formal Analysis of Geometrical Optics in HOL
• Formal verification of stability and chaos in periodic optical systems
• On the formalization of cardinal points of optical systems
• Mathematical aspects of integral optics
• A system approach in the theory of optical spectral measurements

zbMATH Keywords

quantum opticstheorem provingoptical systemscomputer algebra systemselectromagnetic opticsray optics

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Quantum optics (81V80) Electromagnetic theory (general) (78A25) Geometric optics (78A05)

Cites Work

• Title not available (Why is that?)
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Title not available (Why is that?)
• Type classes and filters for mathematical analysis in Isabelle/HOL
• A Skeptic's approach to combining HOL and Maple
• HOL Light: An Overview
• Title not available (Why is that?)
• On the Formal Analysis of Geometrical Optics in HOL
• Formal Analysis of Optical Waveguides in HOL
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• The time to the ancestor along sequences with recombination
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Title not available (Why is that?)
• Single-photon device requirements for operating linear optics quantum computing outside the post-selection basis
• Analytical and computational methods in electromagnetics. With CD-ROM
• Certified Computer Algebra on Top of an Interactive Theorem Prover

Cited In (11)

• Formal verification of stability and chaos in periodic optical systems
• Formal Analysis of Optical Waveguides in HOL
• Formalization of complex vectors in higher-order logic
• Towards the formalization of fractional calculus in higher-order logic
• On the formalization of Fourier transform in higher-order logic
• On the formal analysis of Gaussian optical systems in HOL
• Enabling symbolic and numerical computations in HOL Light
• A Framework for Formal Reasoning about Geometrical Optics
• Formalizing physics: automation, presentation and foundation issues
• On the formalization of cardinal points of optical systems
• Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}

Uses Software

• Matlab
• MuPAD
• Theorema
• ML
• HOL
• HOL Light
• MathDox
• Flyspeck
• CodeV
• Zemax
• MathScheme
• LASCAD
• miz3

This page was built for publication: Formal analysis of optical systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q475384)