{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:16Z","timestamp":1775790796787,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319633893","type":"print"},{"value":"9783319633909","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_1","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Verified Compilation of Space-Efficient Reversible Circuits"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Amy","sequence":"first","affiliation":[]},{"given":"Martin","family":"Roetteler","sequence":"additional","affiliation":[]},{"given":"Krysta M.","family":"Svore","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"1_CR1","unstructured":"Using the GNU Compiler Collection. Free Software Foundation, Inc. (2016). https:\/\/gcc.gnu.org\/onlinedocs\/gcc\/"},{"issue":"6","key":"1_CR2","doi-asserted-by":"publisher","first-page":"818","DOI":"10.1109\/TCAD.2013.2244643","volume":"32","author":"M Amy","year":"2013","unstructured":"Amy, M., Maslov, D., Mosca, M., Roetteler, M.: A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(6), 818\u2013830 (2013)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"1_CR3","unstructured":"Amy, M., Roetteler, M., Svore, K.M.: Verified compilation of space-efficient reversible circuits. arXiv e-prints (2016). https:\/\/arxiv.org\/abs\/1603.01635"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-40578-0_16","volume-title":"Reversible Computation","author":"L Anticoli","year":"2016","unstructured":"Anticoli, L., Piazza, C., Taglialegne, L., Zuliani, P.: Towards quantum programs verification: from quipper circuits to QPMC. In: Devitt, S., Lanese, I. (eds.) RC 2016. LNCS, vol. 9720, pp. 213\u2013219. Springer, Cham (2016). doi:10.1007\/978-3-319-40578-0_16"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1147\/rd.176.0525","volume":"17","author":"CH Bennett","year":"1973","unstructured":"Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. 17, 525\u2013532 (1973)","journal-title":"IBM J. Res. Dev."},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-54833-8_7","volume-title":"Programming Languages and Systems","author":"L Beringer","year":"2014","unstructured":"Beringer, L., Stewart, G., Dockins, R., Appel, A.W.: Verified compilation for shared-memory C. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 107\u2013127. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54833-8_7"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: A verified compiler for an impure functional language. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp. 93\u2013106. ACM (2010)","DOI":"10.1145\/1707801.1706312"},{"key":"1_CR8","unstructured":"Claessen, K.: Embedded languages for describing and verifying hardware. Ph.D. thesis, Chalmers University of Technology and G\u00f6teborg University (2001)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Fournet, C., Swamy, N., Chen, J., Dagand, P.E., Strub, P.Y., Livshits, B.: Fully abstract compilation to JavaScript. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp. 371\u2013384. ACM (2013)","DOI":"10.1145\/2480359.2429114"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Green, A.S., LeFanu Lumsdaine, P., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Proceedings of the 34th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013). ACM (2013)","DOI":"10.1145\/2491956.2462177"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Proceedings of the 28th Annual ACM Symposium on the Theory of Computing (STOC 1996), pp. 212\u2013219. ACM (1996)","DOI":"10.1145\/237814.237866"},{"key":"1_CR12","volume-title":"Partial Evaluation and Automatic Program Generation","author":"ND Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall Inc., Upper Saddle River (1993)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006), pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2564923","volume":"10","author":"CC Lin","year":"2014","unstructured":"Lin, C.C., Jha, N.K.: RMDDS: Reed-Muller decision diagram synthesis of reversible logic circuits. J. Emerg. Technol. Comput. Syst. 10(2), 14 (2014)","journal-title":"J. Emerg. Technol. Comput. Syst."},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1038\/nature13570","volume":"512","author":"IL Markov","year":"2014","unstructured":"Markov, I.L.: Limits on fundamental limits to computation. Nature 512, 147\u2013154 (2014)","journal-title":"Nature"},{"issue":"4","key":"1_CR16","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1278349.1278355","volume":"12","author":"D Maslov","year":"2007","unstructured":"Maslov, D., Miller, D.M., Dueck, G.W.: Techniques for the synthesis of reversible Toffoli networks. ACM Trans. Des. Autom. Electron. Syst. 12(4), 42 (2007)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Miller, D.M., Maslov, D., Dueck, G.W.: A transformation based algorithm for reversible logic synthesis. In: Proceedings of the 40th Annual Design Automation Conference (DAC 2003), pp. 318\u2013323 (2003)","DOI":"10.1145\/775832.775915"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Neis, G., Hur, C.K., Kaiser, J.O., McLaughlin, C., Dreyer, D., Vafeiadis, V.: Pilsner: a compositionally verified compiler for a higher-order imperative language. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 166\u2013178. ACM (2015)","DOI":"10.1145\/2784731.2784764"},{"key":"1_CR19","volume-title":"Quantum Computation and Quantum Information","author":"MA Nielsen","year":"2000","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)"},{"key":"1_CR20","unstructured":"\u00d6mer, B.: Quantum programming in QCL. Master\u2019s thesis, Technical University of Vienna (2000)"},{"key":"1_CR21","unstructured":"Parent, A., Roetteler, M., Svore, K.M.: Reversible circuit compilation with space constraints. arXiv e-prints (2015). https:\/\/arxiv.org\/abs\/1510.00377"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-54833-8_8","volume-title":"Programming Languages and Systems","author":"JT Perconti","year":"2014","unstructured":"Perconti, J.T., Ahmed, A.: Verifying an open compiler using multi-language semantics. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 128\u2013148. Springer, Heidelberg (2014). doi:10.1007\/978-3-642-54833-8_8"},{"issue":"2","key":"1_CR23","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/2431211.2431220","volume":"45","author":"M Saeedi","year":"2013","unstructured":"Saeedi, M., Markov, I.L.: Synthesis and optimization of reversible circuits. ACM Comput. Surv. 45(2), 21 (2013)","journal-title":"ACM Comput. Surv."},{"key":"1_CR24","unstructured":"Scherer, A., Valiron, B., Mau, S.C., Alexander, S., van den Berg, E., Chapuran, T.E.: Resource analysis of the quantum linear system algorithm. arXiv e-prints (2015). https:\/\/arxiv.org\/abs\/1505.06552"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Shafaei, A., Saeedi, M., Pedram, M.: Reversible logic synthesis of $$k$$-input, $$m$$-output lookup tables. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2013), pp. 1235\u20131240 (2013)","DOI":"10.7873\/DATE.2013.256"},{"issue":"5","key":"1_CR26","doi-asserted-by":"publisher","first-page":"1484","DOI":"10.1137\/S0097539795293172","volume":"26","author":"PW Shor","year":"1997","unstructured":"Shor, P.W.: Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM J. Comput. 26(5), 1484\u20131509 (1997)","journal-title":"SIAM J. Comput."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F$$^\\star $$. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 256\u2013270. ACM (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"1_CR28","unstructured":"Thomsen, M.K.: A functional language for describing reversible logic. In: Proceedings of the 2012 Forum on Specification and Design Languages (FDL 2012), pp. 135\u2013142. IEEE (2012)"},{"key":"1_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9579-4","volume-title":"Towards a Design Flow for Reversible Logic","author":"R Wille","year":"2010","unstructured":"Wille, R., Drechsler, R.: Towards a Design Flow for Reversible Logic. Springer, Heidelberg (2010)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Wille, R., Grosse, D., Miller, D., Drechsler, R.: Equivalence checking of reversible circuits. In: Proceedings of the 39th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2009), pp. 324\u2013330 (2009)","DOI":"10.1109\/ISMVL.2009.19"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Wille, R., Offermann, S., Drechsler, R.: Syrec: a programming language for synthesis of reversible circuits. In: Proceedings of the 2010 Forum on Specification and Design Languages (FDL 2010), pp. 1\u20136 (2010)","DOI":"10.1049\/ic.2010.0150"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Yamashita, S., Markov, I.: Fast equivalence-checking for quantum circuits. In: Proceedings of the 2010 IEEE\/ACM Symposium on Nanoscale Architectures (NANOARCH 2010), pp. 23\u201328 (2010)","DOI":"10.1109\/NANOARCH.2010.5510932"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Yokoyama, T., Gl\u00fcck, R.: A reversible programming language and its invertible self-interpreter. In: Proceedings of the 2007 Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2007), pp. 144\u2013153. ACM (2007)","DOI":"10.1145\/1244381.1244404"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:06:54Z","timestamp":1626134814000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}