{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T17:48:07Z","timestamp":1774374487690,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319194578","type":"print"},{"value":"9783319194585","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19458-5_13","type":"book-chapter","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T11:41:14Z","timestamp":1431344474000},"page":"198-211","source":"Crossref","is-referenced-by-count":5,"title":["On the Formal Verification of Optical Quantum Gates in HOL"],"prefix":"10.1007","author":[{"given":"Mohamed Yousri","family":"Mahmoud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Prakash","family":"Panangaden","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Brassard, G., Crepeau, C., Jozsa, R., Langlois, D.: A quantum bit commitment scheme provably unbreakable by both parties. In: Proceedings IEEE Annual Symposium on Foundations of Computer Science, pp. 362\u2013371 (1993)","DOI":"10.1109\/SFCS.1993.366851"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Elleuch, M., Hasan, O., Tahar, S., Abid, M.: Towards the formal performance analysis of wireless sensor networks. In: Proceedings IEEE International Workshop on Enabling Technologies: Infrastructures for Collaborative Enterprises, pp. 365\u2013370 (2013)","DOI":"10.1109\/WETICE.2013.68"},{"key":"13_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":"13_CR5","unstructured":"Griffiths, D.J.: Introduction to Quantum Mechanics. Pearson Prentice Hall (2005)"},{"issue":"4","key":"13_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/j.physrep.2008.09.003","volume":"469","author":"H. Haeffner","year":"2008","unstructured":"Haeffner, H., Roos, C.F., Blatt, R.: Quantum computing with trapped ions. Physics Reports\u00a0469(4), 155\u2013203 (2008)","journal-title":"Physics Reports"},{"issue":"11","key":"13_CR7","first-page":"513","volume":"5","author":"J.A. Jones","year":"2011","unstructured":"Jones, J.A.: Quantum computing: Optical nuclear coupling. Natural Photonics\u00a05(11), 513 (2011)","journal-title":"Natural Photonics"},{"key":"13_CR8","unstructured":"Kolmogorov, A.N., Fomin, S.V., Fomin, S.V.: Elements of the Theory of Functions and Functional Analysis. Dover books on mathematics, vol.\u00a02. Dover (1999)"},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1038\/nature08812","volume":"464","author":"T.D. Ladd","year":"2010","unstructured":"Ladd, T.D., Jelezko, F., Laflamme, R., Nakamura, Y., Monroe, C., O\u2019Brien, J.L.: Quantum computers. Nature\u00a0464, 45\u201353 (2010)","journal-title":"Nature"},{"key":"13_CR10","unstructured":"Lomonaco, S.J.: Quantum Computation: A Grand Mathematical Challenge for the Twenty-first Century and the Millennium. American Mathematical Society (2002)"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1103\/PhysRevA.57.120","volume":"57","author":"D. Loss","year":"1998","unstructured":"Loss, D., DiVincenzo, D.P.: Quantum computation with quantum dots. Physical Review A\u00a057, 120\u2013126 (1998)","journal-title":"Physical Review A"},{"key":"13_CR12","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":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/978-3-319-08970-6_23","volume-title":"Interactive Theorem Proving","author":"M.Y. Mahmoud","year":"2014","unstructured":"Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formal verification of optical quantum flip gate. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol.\u00a08558, pp. 358\u2013373. Springer, Heidelberg (2014)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-319-06200-6_10","volume-title":"NASA Formal Methods","author":"M.Y. Mahmoud","year":"2014","unstructured":"Mahmoud, M.Y., Tahar, S.: On the quantum formalization of coherent light in HOL. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol.\u00a08430, pp. 128\u2013142. Springer, Heidelberg (2014)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Mahmoud, M.Y.: Formal verification of optical quantum gates - HOL Light script (2014), http:\/\/hvg.ece.concordia.ca\/code\/QGates\/","DOI":"10.1007\/978-3-319-19458-5_13"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Mandel, L., Wolf, E.: Optical Coherence and Quantum Optics. Cambridge University Press (1995)","DOI":"10.1017\/CBO9781139644105"},{"key":"13_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-22863-6_18","volume-title":"Interactive Theorem Proving","author":"T. Mhamdi","year":"2011","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: Interactive Theorem Proving. LNCS, vol.\u00a06898, pp. 233\u2013248. Springer, Heidelberg (2011)"},{"key":"13_CR18","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Ralph, T.C., Langford, N.K., Bell, T.B., White, A.G.: Linear optical controlled-not gate in the coincidence basis. Physics Review A\u00a065, 062324 (2002)","DOI":"10.1103\/PhysRevA.65.062324"},{"key":"13_CR20","unstructured":"Verhulst, A.S.: Optical pumping experiments to increase the polarization in nuclear-spin based quantum computers. PhD thesis, Stanford University, CA, USA (2004)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Yamashita, S., Markov, I.L.: Fast equivalence-checking for quantum circuits. In: IEEE\/ACM International Symposium on Nanoscale Architectures, pp. 23\u201328 (2010)","DOI":"10.1109\/NANOARCH.2010.5510932"},{"issue":"12","key":"13_CR22","doi-asserted-by":"publisher","first-page":"1395","DOI":"10.1016\/j.mejo.2008.05.013","volume":"39","author":"M.H. Zaki","year":"2008","unstructured":"Zaki, M.H., Tahar, S., Bois, G.: Formal verification of analog and mixed signal designs: A survey. Microelectronics Journal\u00a039(12), 1395\u20131404 (2008)","journal-title":"Microelectronics Journal"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19458-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T22:49:26Z","timestamp":1748386166000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19458-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194578","9783319194585"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19458-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}