{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:48:58Z","timestamp":1725792538671},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_10","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T05:53:48Z","timestamp":1398232428000},"page":"128-142","source":"Crossref","is-referenced-by-count":7,"title":["On the Quantum Formalization of Coherent Light in HOL"],"prefix":"10.1007","author":[{"given":"Mohamed","family":"Yousri Mahmoud","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1818","key":"10_CR1","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1098\/rspa.1985.0070","volume":"400","author":"D. Deutsch","year":"1985","unstructured":"Deutsch, D.: Quantum theory, the church-turing principle and the universal quantum computer. Proceedings of the Royal Society\u00a0400(1818), 97\u2013117 (1985)","journal-title":"Proceedings of the Royal Society"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Duck, I., Sudarshan, E.C.G.: 100 Years of Planck\u2019s Quantum. World Scientific (2000)","DOI":"10.1142\/4426"},{"key":"10_CR3","unstructured":"Feagin, J.M.: Quantum Methods with Mathematica. Springer (2002)"},{"key":"10_CR4","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/BF02650179","volume":"21","author":"R. Feynman","year":"1982","unstructured":"Feynman, R.: Simulating physics with computers. International Journal of Theoretical Physics\u00a021, 467\u2013488 (1982), doi:10.1007\/BF02650179","journal-title":"International Journal of Theoretical Physics"},{"key":"10_CR5","unstructured":"Institute for Quantum\u00a0Science and Technology at\u00a0the University of Calgary. Introduction to\u00a0an Optical\u00a0lab (2014), \n                  \n                    http:\/\/old.rqc.ru\/quantech\/memo.php"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"issue":"2","key":"10_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J. Harrison","year":"2013","unstructured":"Harrison, J.: The HOL Light Theory of Euclidean Space. Journal of Automated Reasoning\u00a050(2), 173\u2013190 (2013)","journal-title":"Journal of Automated Reasoning"},{"issue":"3-4","key":"10_CR8","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1080\/09500340.2010.546894","volume":"58","author":"T. Jennewein","year":"2011","unstructured":"Jennewein, T., Barbieri, M., White, A.G.: Single-photon device requirements for operating linear optics quantum computing outside the post-selection basis. Journal of Modern Optics\u00a058(3-4), 276\u2013287 (2011)","journal-title":"Journal of Modern Optics"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Li, Y., Browne, D.E., Ch, L.: Kwek, R.\u00a0Raussendorf, and T.\u00a0Wei. Thermal states as universal resources for quantum computation with always-on interactions. Physical Review Letter\u00a0107, 060501 (2011)","DOI":"10.1103\/PhysRevLett.107.060501"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-38088-4_28","volume-title":"NASA Formal Methods","author":"M.Y. Mahmoud","year":"2013","unstructured":"Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 413\u2013427. Springer, Heidelberg (2013)"},{"key":"10_CR11","unstructured":"Mahmoud, M.Y.: On the Quantum Formalization of Coherent Light in HOL - HOL Light script, \n                  \n                    http:\/\/hvg.ece.concordia.ca\/projects\/qoptics\/coh-light.php"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Mandel, L., Wolf, E.: Optical Coherence and Quantum Optics. Cambridge University Press (1995)","DOI":"10.1017\/CBO9781139644105"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Milonni, P., Nieto, M.M.: Coherent states. In: Compendium of Quantum Physics, pp. 106\u2013108. Springer (2009)","DOI":"10.1007\/978-3-540-70626-7_31"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511976667"},{"key":"10_CR15","unstructured":"Institute of\u00a0Quantum Optics at Leibniz University\u00a0of Hannover. General directives for safety in the institute of quantum optics (2014), \n                  \n                    http:\/\/www.iqo.uni-hannover.de\/fileadmin\/institut\/pdf\/job%20security\/3._Sicherheitmerkblatt06012014_engl.pdf"},{"key":"10_CR16","doi-asserted-by":"crossref","first-page":"042319","DOI":"10.1103\/PhysRevA.68.042319","volume":"68","author":"T.C. Ralph","year":"2003","unstructured":"Ralph, T.C., Gilchrist, A., Milburn, G.J., Munro, W.J., Glancy, S.: Quantum computation with optical coherent states. Physical Review A\u00a068, 042319 (2003)","journal-title":"Physical Review A"},{"key":"10_CR17","unstructured":"Santori, C., Fattal, D., Yamamoto, Y.: Single-photon Devices and Applications. Physics textbook. John Wiley & Sons (2010)"},{"issue":"4","key":"10_CR18","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1088\/1464-4266\/1\/4\/312","volume":"1","author":"S.M. Tan","year":"1999","unstructured":"Tan, S.M.: A computational toolbox for quantum and atomic optics. Journal of Optics B: Quantum and Semiclassical Optics\u00a01(4), 424 (1999)","journal-title":"Journal of Optics B: Quantum and Semiclassical Optics"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Walls, D.F., Milburn, G.J.: Quantum Optics. Springer (2008)","DOI":"10.1007\/978-3-540-28574-8"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T17:29:41Z","timestamp":1558891781000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}