{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T23:56:04Z","timestamp":1729641364466,"version":"3.28.0"},"reference-count":16,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1109\/saci.2016.7507376","type":"proceedings-article","created":{"date-parts":[[2016,8,12]],"date-time":"2016-08-12T00:28:06Z","timestamp":1470961686000},"page":"231-236","source":"Crossref","is-referenced-by-count":1,"title":["A case study on algorithm discovery from proofs: The insert function on binary trees"],"prefix":"10.1109","author":[{"given":"Isabela","family":"Dramnesc","sequence":"first","affiliation":[]},{"given":"Tudor","family":"Jebelean","sequence":"additional","affiliation":[]},{"given":"Sorin","family":"Stratulat","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","article-title":"Synthesis of Some Algorithms for Trees: Experiments in Theorema","author":"dramnesc","year":"2015","journal-title":"Technical Report 15–04 RISC Report Series"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/SISY.2015.7325367"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30000-9_43"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45628-7_13"},{"key":"ref14","article-title":"The Art of Computer Programming","volume":"3","author":"knuth","year":"1998","journal-title":"Sorting and Searching"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF00244461"},{"journal-title":"The Mathematica Book","year":"2003","author":"wolfram","key":"ref16"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.006"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-76274-1_8"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.08.003"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2014.09.030"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90029-9"},{"key":"ref2","article-title":"Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions","volume":"xxv","author":"bertot","year":"2004","journal-title":"Texts in Theoretical Computer Science An EATCS"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25951-0_2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2015.30"}],"event":{"name":"2016 IEEE 11th International Symposium on Applied Computational Intelligence and Informatics (SACI)","start":{"date-parts":[[2016,5,12]]},"location":"Timisoara, Romania","end":{"date-parts":[[2016,5,14]]}},"container-title":["2016 IEEE 11th International Symposium on Applied Computational Intelligence and Informatics (SACI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7503033\/7507333\/07507376.pdf?arnumber=7507376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T19:56:51Z","timestamp":1474660611000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7507376\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/saci.2016.7507376","relation":{},"subject":[],"published":{"date-parts":[[2016,5]]}}}