{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T15:10:09Z","timestamp":1748790609123,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319299990"},{"type":"electronic","value":"9783319300009"}],"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-30000-9_43","type":"book-chapter","created":{"date-parts":[[2016,2,25]],"date-time":"2016-02-25T21:45:50Z","timestamp":1456436750000},"page":"562-575","source":"Crossref","is-referenced-by-count":3,"title":["Proof\u2013Based Synthesis of Sorting Algorithms for Trees"],"prefix":"10.1007","author":[{"given":"Isabela","family":"Dr\u0103mnesc","sequence":"first","affiliation":[]},{"given":"Tudor","family":"Jebelean","sequence":"additional","affiliation":[]},{"given":"Sorin","family":"Stratulat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,26]]},"reference":[{"key":"43_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"43_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus","author":"RJ Back","year":"1998","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus. Springer Verlag, New York (1998)"},{"key":"43_CR3","series-title":"Texts in Theoretical Computer Science An EATCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive theorem proving and program development Coq\u2019Art: the calculus of inductive constructions. Texts in Theoretical Computer Science An EATCS, vol. XXV. Springer, Heidelberg (2004)"},{"issue":"4","key":"43_CR4","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4(4), 470\u2013504 (2006)","journal-title":"J. Appl. Logic"},{"key":"43_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.08.003","volume":"153","author":"A Bundy","year":"2006","unstructured":"Bundy, A., Dixon, L., Gow, J., Fleuriot, J.: Constructing induction rules for deductive synthesis proofs. Electron. Notes Theor. Comput. Sci. 153, 3\u201321 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"43_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"C Cohen","year":"2013","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147\u2013162. Springer, Heidelberg (2013)"},{"key":"43_CR7","doi-asserted-by":"crossref","unstructured":"Delaware, B., Claudel, C.P., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp. 689\u2013700. ACM, New York (2015)","DOI":"10.1145\/2775051.2677006"},{"key":"43_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jsc.2014.09.030","volume":"68","author":"I Dramnesc","year":"2015","unstructured":"Dramnesc, I., Jebelean, T.: Synthesis of list algorithms by mechanical proving. J. Symbolic Comput. 68, 61\u201392 (2015)","journal-title":"J. Symbolic Comput."},{"key":"43_CR9","unstructured":"Dramnesc, I., Jebelean, T., Stratulat, S.: Synthesis of some algorithms for trees: experiments in Theorema. Technical report 15\u201304, RISC Report Series, Johannes Kepler University, Linz, Austria (2015)"},{"key":"43_CR10","doi-asserted-by":"crossref","unstructured":"Dramnesc, I., Jebelean, T., Stratulat, S.: Theory exploration of binary trees. In: 13th IEEE International Symposium on Intelligent Systems and Informatics (SISY 2015), pp. 139\u2013144. IEEE Publishing (2015)","DOI":"10.1109\/SISY.2015.7325367"},{"key":"43_CR11","doi-asserted-by":"crossref","unstructured":"Dramnesc, I., Jebelean, T., Stratulat, S.: Combinatorial techniques for proof-based synthesis of sorting algorithms. In: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015 (to appear)","DOI":"10.1109\/SYNASC.2015.30"},{"key":"43_CR12","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2010, pp. 13\u201324. ACM, New York (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"43_CR13","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2013, pp. 407\u2013426. ACM, New York (2013)","DOI":"10.1145\/2544173.2509555"},{"key":"43_CR14","volume-title":"The Art of Computer Programming, Volume 3: Sorting and Searching","author":"DE Knuth","year":"1998","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 3: Sorting and Searching, 2nd edn. Addison Wesley Longman Publishing, Redwood City (1998)","edition":"2"},{"key":"43_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"43_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-69149-5_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"DR Smith","year":"2008","unstructured":"Smith, D.R.: Generating programs plus proofs by refinement. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 182\u2013188. Springer, Heidelberg (2008)"},{"key":"43_CR17","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: A unified view of induction reasoning for first-order logic. In: Voronkov, A. (ed.) Turing-100 (The Alan Turing Centenary Conference). EPiC Series, vol. 10, pp. 326\u2013352. EasyChair (2012)","DOI":"10.29007\/nsx4"},{"key":"43_CR18","doi-asserted-by":"crossref","unstructured":"Stratulat, S.: Mechanically certifying formula-based noetherian induction reasoning. J. Symbolic Comput. (accepted). http:\/\/lita.univ-lorraine.fr\/~stratula\/jsc2016.pdf","DOI":"10.1016\/j.jsc.2016.07.014"},{"issue":"4","key":"43_CR19","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM 14(4), 221\u2013227 (1971)","journal-title":"Commun. ACM"},{"key":"43_CR20","volume-title":"The Mathematica Book","author":"S Wolfram","year":"2003","unstructured":"Wolfram, S.: The Mathematica Book. Wolfram Media Inc., Champaign (2003)"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30000-9_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:36:36Z","timestamp":1748788596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30000-9_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319299990","9783319300009"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30000-9_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}