{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T16:40:43Z","timestamp":1761324043525},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Optics technology is being increasingly used in mainstream industrial and research domains such as terrestrial telescopes, biomedical imaging and optical communication. One of the most widely used modeling approaches for such systems is Gaussian optics, which describes light as a beam. In this paper, we propose to use higher-order-logic theorem proving for the analysis of Gaussian optical systems. In particular, we present the formalization of Gaussian beams and verify the corresponding properties such as beam transformation, beam waist radius and location. Consequently, we build formal reasoning support for the analysis of quasi-optical systems. In order to demonstrate the effectiveness of our approach, we present a case study about the receiver module of a real-world Atacama Pathfinder Experiment (APEX) telescope.<\/jats:p>","DOI":"10.1007\/s00165-016-0367-1","type":"journal-article","created":{"date-parts":[[2016,3,18]],"date-time":"2016-03-18T15:18:12Z","timestamp":1458314292000},"page":"881-907","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the formal analysis of Gaussian optical systems in HOL"],"prefix":"10.1145","volume":"28","author":[{"given":"Umair","family":"Siddique","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Avigad J Donnelly K (2004) Formalizing O notation in Isabelle\/HOL. In: Automated reasoning Lecture Notes in Computer Science vol 3097. Springer Berlin Heidelberg pp 357\u2013371","DOI":"10.1007\/978-3-540-25984-8_27"},{"key":"e_1_2_1_2_2_2","unstructured":"Atacama Pathfinder EXperiment (APEX) (2015) http:\/\/www.apex-telescope.org\/"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0175-z"},{"key":"e_1_2_1_2_4_2","unstructured":"Chabory A Sokoloff J Bolioli S Elis K (2010) Application of gaussian beam based techniques to the quasi-optical systems of radiofrequency radiometers. In: European Conference on Antennas and Propagation vol 2010 pp 12\u201316"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Damask JN (2005) Polarization optics in telecommunications. Springer Series in Optical Sciences. Springer","DOI":"10.1007\/b137386"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Franke-Arnold S Gay SJ Puthoor IV (2013) Quantum process calculus for linear optical quantum computing. In: Reversible Computation Lecture Notes in Computer Science vol 7948. Springer pp 234\u2013246","DOI":"10.1007\/978-3-642-38986-3_19"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Fleuriot JD (2001) Nonstandard geometric proofs. In: Automated deduction in geometry Lecture Notes in Computer Science vol 2061. Springer pp 246\u2013267","DOI":"10.1007\/3-540-45410-1_15"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Goldsmith PF (1998) Quasioptical systems: gaussian beam quasioptical propogation and applications. IEEE Press Series on RF and Microwave Technology. Wiley","DOI":"10.1109\/9780470546291"},{"key":"e_1_2_1_2_9_2","unstructured":"Griffiths DJ (2005) Introduction to quantum mechanics. Pearson Prentice Hall"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press","DOI":"10.1017\/CBO9780511576430"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Harrison J (2009) HOL light: an overview. In: Theorem Proving in Higher Order Logics Lecture Notes in Computer Science vol 5674. Springer pages 60\u201366","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"e_1_2_1_2_13_2","unstructured":"Hodgson N Weber H (2005) Optical resonators: fundamentals advanced concepts applications. Springer Series in Optical Sciences. Springer"},{"key":"e_1_2_1_2_14_2","unstructured":"Hodgson N Weber H (2005) Optical resonators: fundamentals advanced concepts applications. Springer"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Khan-Afshar S Hasan O Tahar S (2014) Formal analysis of electromagnetic optics. In: Novel optical systems design and optimization SPIE vol 9193 pp 91930A\u201391930A\u201314","DOI":"10.1117\/12.2062965"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1364\/AO.5.001550"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9303-3"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Kaliszyk C Urban J Siddique U Khan-Afshar S Dunchev C Tahar S (2015) Formalizing physics: automation presentation and foundation issues. In: Intelligent computer mathematics Lecture Notes in Computer Science vol 9150. Springer pp 288\u2013295","DOI":"10.1007\/978-3-319-20615-8_19"},{"key":"e_1_2_1_2_19_2","unstructured":"LASCAD (2015) http:\/\/www.las-cad.com\/"},{"issue":"016611","key":"e_1_2_1_2_20_2","first-page":"1","article-title":"Analysis of optical pulse propagation with two-by-two (ABCD) matrices","volume":"64","author":"Mookherjea S","year":"2001","journal-title":"Phys Rev E."},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Malak M Pavy N Marty F Peter Y Liu AQ Bourouina T (2011) Stable high-Q fabry-perot resonators with long cavity based on curved all-silicon high reflectance mirrors. In: IEEE international conference on micro electro mechanical systems pp 720\u2013723","DOI":"10.1109\/MEMSYS.2011.5734526"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Mahmoud MY Tahar S (2014) On the quantum formalization of coherent light in HOL. In: NASA formal methods LNCS vol 8430. Springer pp 128\u2013142","DOI":"10.1007\/978-3-319-06200-6_10"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/3.687847"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10762-009-9493-7"},{"key":"e_1_2_1_2_25_2","unstructured":"Optica (2015) http:\/\/www.opticasoftware.com\/"},{"key":"e_1_2_1_2_26_2","unstructured":"reZonator (2015) http:\/\/www.rezonator.orion-project.org\/"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Siddique U Aravantinos V Tahar S (2013) Formal stability analysis of optical resonators. In: NASA formal methods Lecture Notes in Computer Science vol 7871 pp 368\u2013382","DOI":"10.1007\/978-3-642-38088-4_25"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Siddique U Aravantinos V Tahar S (2013) On the formal analysis of geometrical optics in HOL. In: Automated deduction in geometry Lecture Notes in Computer Science vol 7993 pp 161\u2013180","DOI":"10.1007\/978-3-642-40672-0_11"},{"key":"e_1_2_1_2_29_2","unstructured":"Siddique U (2015) Formal analysis of gaussian optical systems: source code. http:\/\/hvg.ece.concordia.ca\/projects\/optics\/gaussian.html"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Saleh BEA Teich MC (2007) Fundamentals of photonics. Wiley","DOI":"10.1117\/1.2976006"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.optlastec.2011.03.031"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1063\/1.2387965"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Tr\u00e4ger F (2007) Handbook of lasers and optics. Springer.","DOI":"10.1007\/978-0-387-30420-5"},{"key":"e_1_2_1_2_34_2","unstructured":"Wilson WC Atkinson GM (2005) MOEMS modeling using the geometrical matrix toolbox. Technical report NASA Langley Research Center"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Wellner M (1991) Wave optics. In: Elements of physics pp 543\u2013575. Springer","DOI":"10.1007\/978-1-4615-3860-8_24"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0367-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0367-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0367-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,15]],"date-time":"2024-06-15T03:06:30Z","timestamp":1718420790000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0367-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":35,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["10.1007\/s00165-016-0367-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0367-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}