{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:46:19Z","timestamp":1761648379113,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319405773"},{"type":"electronic","value":"9783319405780"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40578-0_21","type":"book-chapter","created":{"date-parts":[[2016,6,29]],"date-time":"2016-06-29T20:25:20Z","timestamp":1467231920000},"page":"289-306","source":"Crossref","is-referenced-by-count":2,"title":["Generating Reversible Circuits from Higher-Order Functional Programs"],"prefix":"10.1007","author":[{"given":"Beno\u00eet","family":"Valiron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,30]]},"reference":[{"issue":"3","key":"21_CR1","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/j.tcs.2005.07.002","volume":"347","author":"S Abramsky","year":"2005","unstructured":"Abramsky, S.: A structural approach to reversible computation. Theor. Comput. Sci. 347(3), 441\u2013464 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR2","doi-asserted-by":"crossref","first-page":"2513","DOI":"10.1137\/080712167","volume":"39","author":"A Ambainis","year":"2010","unstructured":"Ambainis, A., Childs, A.M., et al.: Any AND-OR formula of size $$n$$ can be evaluated in time $$n^{\\frac{1}{2}+o(1)}$$ on a quantum computer. SIAM J. Comput. 39, 2513\u20132530 (2010)","journal-title":"SIAM J. Comput."},{"key":"21_CR3","doi-asserted-by":"crossref","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":"21_CR4","doi-asserted-by":"crossref","unstructured":"Berry, G.: The foundations of esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner. MIT Press, Cambridge (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-3-642-39799-8_14","volume-title":"Computer Aided Verification","author":"T Braibant","year":"2013","unstructured":"Braibant, T., Chlipala, A.: Formal verification of hardware synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 213\u2013228. Springer, Heidelberg (2013)"},{"key":"21_CR6","unstructured":"Claessen, K.: Embedded languages for describing and verifying hardware. Ph.D. thesis, Chalmers University of Technology and G\u00f6teborg University (2001)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Fazel, K., Thornton, M.A., Rice, J.E.: ESOP-based Toffoli gate cascade generation. In: Proceedings of PacRim, pp. 206\u2013209 (2007)","DOI":"10.1109\/PACRIM.2007.4313212"},{"key":"21_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1364\/ON.11.2.000011","volume":"11","author":"RP Feynman","year":"1985","unstructured":"Feynman, R.P.: Quantum mechanical computers. Optics News 11, 11\u201320 (1985)","journal-title":"Optics News"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Ghica, D.R.: Geometry of synthesis. In: Proceedings of POPL, pp. 363\u2013375 (2007)","DOI":"10.1145\/1190216.1190269"},{"key":"21_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1090\/conm\/092\/1003197","volume":"92","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y.: Towards a geometry of interaction. Contemp. Math. 92, 69\u2013108 (1989)","journal-title":"Contemp. Math."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Green, A.S., Lumsdaine, P.L., et al.: Quipper: a scalable quantum programming language. In: Proceedings of PLDI, pp. 333\u2013342 (2013)","DOI":"10.1145\/2491956.2462177"},{"issue":"11","key":"21_CR12","doi-asserted-by":"crossref","first-page":"2317","DOI":"10.1109\/TCAD.2006.871622","volume":"25","author":"P Gupta","year":"2006","unstructured":"Gupta, P., Agrawal, A., Jha, N.K.: An algorithm for synthesis of reversible logic circuits. IEEE Trans. CAD Int. Circ. Syst. 25(11), 2317\u20132330 (2006)","journal-title":"IEEE Trans. CAD Int. Circ. Syst."},{"issue":"15","key":"21_CR13","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1103\/PhysRevLett.103.150502","volume":"103","author":"AW Harrow","year":"2009","unstructured":"Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Phys. Rev. Lett. 103(15), 150\u2013502 (2009)","journal-title":"Phys. Rev. Lett."},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"James, R.P., Sabry, A.: Information effects. In: Proceedings of POPL, pp. 73\u201384 (2012)","DOI":"10.1145\/2103656.2103667"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","first-page":"95","volume-title":"Implementation of Functional Languages","author":"W Kluge","year":"1999","unstructured":"Kluge, W.: A reversible SE(M)CD machine. IFL\u201999. LNCS, vol. 1868, pp. 95\u2013113. Springer, Heidelberg (1999)"},{"key":"21_CR16","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1147\/rd.53.0261","volume":"5","author":"R Laundauer","year":"1961","unstructured":"Laundauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5, 261\u2013269 (1961)","journal-title":"IBM J. Res. Dev."},{"issue":"2","key":"21_CR17","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1137\/050643684","volume":"37","author":"F Magniez","year":"2007","unstructured":"Magniez, F., Santha, M., Szegedy, M.: Quantum algorithms for the triangle problem. SIAM J. Comput. 37(2), 413\u2013424 (2007)","journal-title":"SIAM J. Comput."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Maslov, D., Dueck, G W., Miller, D.M.: Fredkin\/Toffoli templates for reversible logic synthesis. In: Proceedings of ICCAD, pp. 256\u2013261 (2003)","DOI":"10.1109\/ICCAD.2003.1257667"},{"key":"21_CR19","volume-title":"Quantum Computation and Quantum Information","author":"MA Nielsen","year":"2002","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge Univ. Press, Cambridge (2002)"},{"key":"21_CR20","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-1-4020-8588-8_8","volume-title":"High-Level Synthesis","author":"RS Nikhil","year":"2008","unstructured":"Nikhil, R.S.: Bluespec: a general-purpose approach to high-level synthesis based on parallel atomic transactions. In: Coussy, P., Morawiec, A. (eds.) High-Level Synthesis, pp. 129\u2013146. Springer, Heidelberg (2008)"},{"key":"21_CR21","unstructured":"Parent, A., Roetteler, M., Svore, K.M.: Reversible circuit compilation with space constraints. arXiv:1510.00377 (2015)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Park, S., Kim, J., Im, H.: Functional netlists. In: Proceedings of ICFP, pp. 353\u2013366 (2008)","DOI":"10.1145\/1411204.1411253"},{"key":"21_CR23","unstructured":"Quipper. http:\/\/www.mathstat.dal.ca\/~selinger\/quipper\/"},{"issue":"2","key":"21_CR24","doi-asserted-by":"crossref","first-page":"21:1","DOI":"10.1145\/2431211.2431220","volume":"45","author":"M Saeedi","year":"2013","unstructured":"Saeedi, M., Markov, I.L.: Synthesis and optimization of reversible circuits - a survey. ACM Comput. Surv. 45(2), 21:1\u201321:34 (2013)","journal-title":"ACM Comput. Surv."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Sanaee, Y., Saeedi, M., Zamani, M.S.:Shared-PPRM: a memory-efficient representation for boolean reversiblefunctions. In: Proceedings of ISVLSI, pp. 471\u2013474 (2008)","DOI":"10.1109\/ISVLSI.2008.41"},{"key":"21_CR26","unstructured":"Sander, I.: System modeling and design refinement in ForSyDe. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2003)"},{"key":"21_CR27","unstructured":"Scherer, A., Valiron, B., et al.: Resource analysis of the quantum linear system algorithm. arxiv:1505.06552 (2015)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Shor, P.: Algorithms for quantum computation: discrete logarithm and factoring. In: Proceedings of FOCS (1994)","DOI":"10.1109\/SFCS.1994.365700"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1007\/978-3-642-29517-1_6","volume-title":"Reversible Computation","author":"M Soeken","year":"2012","unstructured":"Soeken, M., Frehse, S., Wille, R., Drechsler, R.: RevKit: an open source toolkit for the design of reversible circuits. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 64\u201376. Springer, Heidelberg (2012)"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-642-36678-9","volume-title":"Reversible Computation","author":"AS Green","year":"2013","unstructured":"Green, A.S., Lumsdaine, P.L.F., Ross, N.J., Selinger, P., Valiron, B.: White dots do matter: rewriting reversible logic circuits. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 196\u2013208. Springer, Heidelberg (2013)"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Swamy, N., Guts, N., et al.: Lightweight monadic programming in ML. In: Proceedings of ICFP, pp. 15\u201327 (2011)","DOI":"10.1145\/2034773.2034778"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Terui, K.: Proof nets and boolean circuits. In: Proceedings of LICS, pp. 182\u2013191 (2004)","DOI":"10.1109\/LICS.2004.1319612"},{"key":"21_CR33","unstructured":"Thomsen, M.K.: A functional language for describing reversible logic. In: Proceedings of FDL, pp. 135\u2013142 (2012)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Wille, R., Gro\u00dfe, D., et al.: RevLib: an online resource for reversible functions and reversible circuits. In: International Symposium on Multi-valued Logic, pp. 220\u2013225 (2008)","DOI":"10.1109\/ISMVL.2008.43"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Wille, R., Le, H.M., Dueck, G.W., Grosse, D.: Quantified synthesis of reversible logic. In: Proceedings of DATE, pp. 1015\u20131020 (2008)","DOI":"10.1109\/DATE.2008.4484814"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Wille, R., Offermann, S., Drechsler, R.:SyReC: a programming language for synthesis of reversible circuits. In: Forum on Specification Design Languages, pp. 1\u20136 (2010)","DOI":"10.1049\/ic.2010.0150"}],"container-title":["Lecture Notes in Computer Science","Reversible Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40578-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T23:14:45Z","timestamp":1748992485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40578-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319405773","9783319405780"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40578-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}