Formal analysis of optical systems
From MaRDI portal
Publication:475384
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.
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
Cites work
- scientific article; zbMATH DE number 3141869 (Why is no real title available?)
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 1254246 (Why is no real title available?)
- scientific article; zbMATH DE number 1259143 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Skeptic's approach to combining HOL and Maple
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Analytical and computational methods in electromagnetics. With CD-ROM
- Certified Computer Algebra on Top of an Interactive Theorem Prover
- Formal Analysis of Optical Waveguides in HOL
- HOL Light: An Overview
- On the Formal Analysis of Geometrical Optics in HOL
- Single-photon device requirements for operating linear optics quantum computing outside the post-selection basis
- The time to the ancestor along sequences with recombination
- Theorem Proving in Higher Order Logics
- Type classes and filters for mathematical analysis in Isabelle/HOL
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
Cited in
(11)- A Framework for Formal Reasoning about Geometrical Optics
- Towards the formalization of fractional calculus in higher-order logic
- Formal verification of stability and chaos in periodic optical systems
- On the formalization of cardinal points of optical systems
- Formalization of complex vectors in higher-order logic
- Enabling symbolic and numerical computations in HOL Light
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}
- Formal Analysis of Optical Waveguides in HOL
- On the formalization of Fourier transform in higher-order logic
- On the formal analysis of Gaussian optical systems in HOL
- Formalizing physics: automation, presentation and foundation issues
Describes a project that uses
Uses Software
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)
