On the formal analysis of Gaussian optical systems in HOL

DOI10.1007/s00165-016-0367-1zbMath1345.78002OpenAlexW2334113034MaRDI QIDQ315313

Sofiène Tahar, Umair Siddique

Publication date: 20 September 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-016-0367-1

zbMATH Keywords

theorem provinggeometrical opticsGaussian beamsHOL Lightquasi-optical systems

Mathematics Subject Classification ID

Uses Software

• HOL Light
• Flyspeck

Cites Work

• Unnamed Item
• Unnamed Item
• Formal analysis of optical systems
• The HOL Light theory of Euclidean space
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• On the Formal Analysis of Geometrical Optics in HOL
• Quantum Process Calculus for Linear Optical Quantum Computing
• HOL Light: An Overview
• Formalizing Physics: Automation, Presentation and Foundation Issues
• Automated Reasoning

This page was built for publication: On the formal analysis of Gaussian optical systems in HOL