{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:12:26Z","timestamp":1725862346850},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662529201"},{"type":"electronic","value":"9783662529218"}],"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-662-52921-8_4","type":"book-chapter","created":{"date-parts":[[2016,8,5]],"date-time":"2016-08-05T11:22:30Z","timestamp":1470396150000},"page":"52-67","source":"Crossref","is-referenced-by-count":0,"title":["A Classical Propositional Logic for Reasoning About Reversible Logic Circuits"],"prefix":"10.1007","author":[{"given":"Holger Bock","family":"Axelsen","sequence":"first","affiliation":[]},{"given":"Robert","family":"Gl\u00fcck","sequence":"additional","affiliation":[]},{"given":"Robin","family":"Kaarsgaard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,6]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Arabzadeh, M., Saeedi, M., Zamani, M.S.: Rule-based optimization of reversible circuits. In: Proceedings of the ASP-DAC 2010, pp. 849\u2013854. IEEE (2010)","DOI":"10.1109\/ASPDAC.2010.5419684"},{"issue":"7388","key":"4_CR2","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1038\/nature10872","volume":"483","author":"A B\u00e9rut","year":"2012","unstructured":"B\u00e9rut, A., Arakelyan, A., Petrosyan, A., Ciliberto, S., Dillenschneider, R., Lutz, E.: Experimental verification of Landauer\u2019s principle linking information and thermodynamics. Nature 483(7388), 187\u2013189 (2012)","journal-title":"Nature"},{"key":"4_CR3","volume-title":"Handbook of Proof Theory","author":"SR Buss","year":"1998","unstructured":"Buss, S.R.: Handbook of Proof Theory. Elsevier, Amsterdam (1998)"},{"key":"4_CR4","doi-asserted-by":"crossref","DOI":"10.1002\/9783527633999","volume-title":"Reversible Computing","author":"A Vos De","year":"2010","unstructured":"De Vos, A.: Reversible Computing. Wiley-VCH, Weinheim (2010)"},{"issue":"2","key":"4_CR5","first-page":"11:1","volume":"11","author":"A Vos De","year":"2014","unstructured":"De Vos, A., Burignat, S., Gl\u00fcck, R., Mogensen, T.\u00c6., Axelsen, H.B., Thomsen, M.K., Rotenberg, E., Yokoyama, T.: Designing garbage-free reversible implementations of the integer cosine transform. ACM J. Emerg. Tech. Com. 11(2), 11:1\u201311:15 (2014)","journal-title":"ACM J. Emerg. Tech. Com."},{"issue":"6","key":"4_CR6","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1007\/BF01886518","volume":"16","author":"RP Feynman","year":"1986","unstructured":"Feynman, R.P.: Quantum mechanical computers. Found. Phys. 16(6), 507\u2013531 (1986)","journal-title":"Found. Phys."},{"key":"4_CR7","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)"},{"issue":"15\u201316","key":"4_CR8","first-page":"1302","volume":"14","author":"SP Jordan","year":"2014","unstructured":"Jordan, S.P.: Strong equivalence of reversible circuits is coNP-complete. Quantum Inf. Comput. 14(15\u201316), 1302\u20131307 (2014)","journal-title":"Quantum Inf. Comput."},{"issue":"1","key":"4_CR9","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0001-8708(91)90003-P","volume":"88","author":"A Joyal","year":"1991","unstructured":"Joyal, A., Street, R.: The geometry of tensor calculus I. Adv. Math. 88(1), 55\u2013112 (1991)","journal-title":"Adv. Math."},{"issue":"1","key":"4_CR10","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1006\/aima.1993.1055","volume":"102","author":"A Joyal","year":"1993","unstructured":"Joyal, A., Street, R.: Braided tensor categories. Adv. Math. 102(1), 20\u201378 (1993)","journal-title":"Adv. Math."},{"key":"4_CR11","unstructured":"Kaarsgaard, R.: Towards a propositional logic for reversible logic circuits. In: Proceedings of the ESSLLI 2014 Student Session, pp. 33\u201341 (2014). http:\/\/www.kr.tuwien.ac.at\/drm\/dehaan\/stus2014\/proceedings.pdf"},{"issue":"3","key":"4_CR12","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1147\/rd.53.0183","volume":"5","author":"R Landauer","year":"1961","unstructured":"Landauer, R.: Irreversibility and heat generation in the computing process. IBM J. Res. Dev. 5(3), 261\u2013269 (1961)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR13","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511525896","volume-title":"Higher Operads, Higher Categories","author":"T Leinster","year":"2004","unstructured":"Leinster, T.: Higher Operads, Higher Categories. London Mathematical Society Lecture Note Series, vol. 298. Cambridge University Press, Cambridge (2004)"},{"key":"4_CR14","doi-asserted-by":"crossref","first-page":"06FE10","DOI":"10.7567\/JJAP.51.06FE10","volume":"51","author":"AO Orlov","year":"2012","unstructured":"Orlov, A.O., Lent, C.S., Thorpe, C.C., Boechler, G.P., Snider, G.L.: Experimental test of Landauer\u2019s principle at the sub- $$k_{\\rm {b}} t$$ level. Japan. J. Appl. Phys. 51, 06FE10 (2012)","journal-title":"Japan. J. Appl. Phys."},{"key":"4_CR15","unstructured":"Polakow, J.: Ordered linear logic and applications. Ph.D. thesis, CMU (2001)"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Rendel, T., Ostermann, K.: Invertible syntax descriptions: unifying parsing and pretty printing. ACM SIGPLAN Notices, vol. 45, No. 11, pp. 1\u201312 (2010)","DOI":"10.1145\/2088456.1863525"},{"issue":"1","key":"4_CR17","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.jlap.2009.02.006","volume":"79","author":"MP Schellekens","year":"2010","unstructured":"Schellekens, M.P.: MOQA: unlocking the potential of compositional static average-case analysis. J. Log. Algebr. Program. 79(1), 61\u201383 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1090\/conm\/092\/1003210","volume":"92","author":"RAG Seely","year":"1989","unstructured":"Seely, R.A.G.: Linear logic, *-autonomous categories and cofree coalgebras. Contemp. Math. 92, 371\u2013382 (1989)","journal-title":"Contemp. Math."},{"key":"4_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-85820-8","volume-title":"Boolean Algebras","author":"R Sikorski","year":"1969","unstructured":"Sikorski, R.: Boolean Algebras. Springer, Heidelberg (1969)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-642-38986-3_16","volume-title":"Reversible Computation","author":"M Soeken","year":"2013","unstructured":"Soeken, M., Thomsen, M.K.: 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)"},{"issue":"38","key":"4_CR21","doi-asserted-by":"crossref","first-page":"382002","DOI":"10.1088\/1751-8113\/43\/38\/382002","volume":"43","author":"MK Thomsen","year":"2010","unstructured":"Thomsen, M.K., Gl\u00fcck, R., Axelsen, H.B.: Reversible arithmetic logic unit for quantum arithmetic. J. Phys. A Math. Theor. 43(38), 382002 (2010)","journal-title":"J. Phys. A Math. Theor."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1007\/3-540-10003-2_104","volume-title":"Automata, Languages and Programming","author":"T Toffoli","year":"1980","unstructured":"Toffoli, T.: Reversible computing. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 632\u2013644. Springer, Heidelberg (1980)"},{"key":"4_CR23","doi-asserted-by":"crossref","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)"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-52921-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:04:03Z","timestamp":1498320243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-52921-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662529201","9783662529218"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-52921-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}