{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:55:24Z","timestamp":1725900924184},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642380877"},{"type":"electronic","value":"9783642380884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_28","type":"book-chapter","created":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T00:38:27Z","timestamp":1368059907000},"page":"413-427","source":"Crossref","is-referenced-by-count":13,"title":["Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory"],"prefix":"10.1007","author":[{"given":"Mohamed Yousri","family":"Mahmoud","sequence":"first","affiliation":[]},{"given":"Vincent","family":"Aravantinos","sequence":"additional","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Aladev, V.Z.: Computer Algebra Systems: A New Software Toolbox For Maple. Computer Mathematics Series. Fultus Books (2004)","DOI":"10.1007\/3-540-44860-8_73"},{"key":"28_CR2","unstructured":"Bakshi, U.A., Bakshi, V.: Modern Control Theory. Technical Publications (2009)"},{"issue":"5","key":"28_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/gmip.1997.0425","volume":"59","author":"S. Chandrasekaran","year":"1997","unstructured":"Chandrasekaran, S., Manjunath, B.S., Wang, Y.F., Winkeler, J., Zhang, H.: An Eigenspace Update Algorithm for Image Analysis. Graphical Models and Image Processing\u00a059(5), 321\u2013332 (1997)","journal-title":"Graphical Models and Image Processing"},{"key":"28_CR4","unstructured":"Dettman, J.W.: Introduction to Linear Algebra. Dover Books on Mathematics Series. Dover (1974)"},{"key":"28_CR5","unstructured":"Fox, M.: Quantum Optics: An Introduction. Oxford Master Series in Physics. Oxford University Press (2006)"},{"key":"28_CR6","unstructured":"Griffiths, D.J.: Introduction to Quantum Mechanics. Pearson Prentice Hall (2005)"},{"key":"28_CR7","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)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL Theory of Euclidean Space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-28891-3_15","volume-title":"NASA Formal Methods","author":"H. Herencia-Zapana","year":"2012","unstructured":"Herencia-Zapana, H., Jobredeaux, R., Owre, S., Garoche, P.-L., Feron, E., Perez, G., Ascariz, P.: PVS linear algebra libraries for verification of control software algorithms in C\/ACSL. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 147\u2013161. Springer, Heidelberg (2012)"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"Hirvensalo, M.: Quantum Computing. Natural Computing Series. Springer (2004)","DOI":"10.1007\/978-3-662-09636-9"},{"key":"28_CR11","unstructured":"Stein. J.: http:\/\/coq.inria.fr\/pylons\/contribs\/view\/LinAlg\/trunk"},{"key":"28_CR12","unstructured":"Khan Afshar, S., Aravantinos, V.: http:\/\/hvg.ece.concordia.ca\/code\/hol-light\/complex-vectors"},{"issue":"7","key":"28_CR13","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1088\/0034-4885\/66\/7\/203","volume":"66","author":"U. Leonhardt","year":"2003","unstructured":"Leonhardt, U.: Quantum Physics of Simple Optical Instruments. Reports on Progress in Physics\u00a066(7), 1207 (2003)","journal-title":"Reports on Progress in Physics"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Leonhardt, U.: Essential Quantum Optics: From Quantum Measurements to Black Holes. Cambridge University Press (2010)","DOI":"10.1017\/CBO9780511806117"},{"key":"28_CR15","unstructured":"Mahmoud, M.Y., Aravantinos, V.: http:\/\/hvg.ece.concordia.ca\/code\/hol-light\/qoptics\/qalgebra.ml"},{"key":"28_CR16","unstructured":"The Coq development team: The Coq Proof Assistant Reference Manual. LogiCal Project, Version 8.0 (2004)"},{"key":"28_CR17","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":"28_CR18","doi-asserted-by":"crossref","unstructured":"Strang, G.: Introduction to Linear Algebra. Wellsley-Cambrige Press (2003)","DOI":"10.1007\/978-3-642-55631-9"},{"issue":"4","key":"28_CR19","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1093\/bioinformatics\/btg005","volume":"19","author":"S. Vinga","year":"2003","unstructured":"Vinga, S., Almeida, J.: Alignment-Free Sequence Comparison \u2013 A Review. Bioinformatics\u00a019(4), 513\u2013523 (2003)","journal-title":"Bioinformatics"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,16]],"date-time":"2022-02-16T14:42:12Z","timestamp":1645022532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}