{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:42:20Z","timestamp":1770835340209,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,3,24]],"date-time":"2014-03-24T00:00:00Z","timestamp":1395619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Conseil General du Loiret"},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["10102704"],"award-info":[{"award-number":["10102704"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-2010-INTB-0205-02"],"award-info":[{"award-number":["ANR-2010-INTB-0205-02"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,3,24]]},"DOI":"10.1145\/2554850.2554912","type":"proceedings-article","created":{"date-parts":[[2014,7,22]],"date-time":"2014-07-22T15:08:30Z","timestamp":1406041710000},"page":"1577-1584","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal derivation and extraction of a parallel program for the all nearest smaller values problem"],"prefix":"10.1145","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"first","affiliation":[{"name":"Univ Orl\u00e9ans, Orl\u00e9ans, France"}]},{"given":"Simon","family":"Robillard","sequence":"additional","affiliation":[{"name":"Univ Orl\u00e9ans, Orl\u00e9ans, France"}]},{"given":"Julien","family":"Tesson","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Est, LACL, UPEC, France"}]},{"given":"Joeffrey","family":"Legaux","sequence":"additional","affiliation":[{"name":"Univ Orl\u00e9ans, LIFO EA, Orl\u00e9ans, France"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"}]}],"member":"320","published-online":{"date-parts":[[2014,3,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/jagm.1993.1018"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/248932"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCC.2010.23"},{"key":"e_1_3_2_1_4_1","volume-title":"Algorithmic Skeletons: Structured Management of Parallel Computation","author":"Cole M.","year":"1989","unstructured":"M. Cole . Algorithmic Skeletons: Structured Management of Parallel Computation . MIT Press , 1989 . Available at http:\/\/homepages.inf.ed.ac.uk\/mic\/Pubs. M. Cole. Algorithmic Skeletons: Structured Management of Parallel Computation. MIT Press, 1989. Available at http:\/\/homepages.inf.ed.ac.uk\/mic\/Pubs."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626495000175"},{"key":"e_1_3_2_1_6_1","volume-title":"C\/C++ Verification Workshop","author":"Daum M.","year":"2007","unstructured":"M. Daum . Reasoning on Data-Parallel Programs in Isabelle\/Hol . In C\/C++ Verification Workshop , 2007 . M. Daum. Reasoning on Data-Parallel Programs in Isabelle\/Hol. In C\/C++ Verification Workshop, 2007."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122980"},{"key":"e_1_3_2_1_8_1","series-title":"Procedia Computer Science","first-page":"1837","volume-title":"ICCS","author":"Di Cosmo R.","year":"2012","unstructured":"R. Di Cosmo and M. Danelutto . A \"minimal disruption\" skeleton experiment: seamless map & reduce embedding in OCaml . In ICCS , volume 9 of Procedia Computer Science , pages 1837 -- 1846 . Elsevier , 2012 . R. Di Cosmo and M. Danelutto. A \"minimal disruption\" skeleton experiment: seamless map & reduce embedding in OCaml. In ICCS, volume 9 of Procedia Computer Science, pages 1837--1846. Elsevier, 2012."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_24"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770379"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDCAT.2010.86"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.2001.1741"},{"key":"e_1_3_2_1_13_1","volume-title":"Algebraic laws for BSP programming","author":"Jifeng H.","year":"1996","unstructured":"H. Jifeng , Q. Miller , and L. Chen . Algebraic laws for BSP programming . In L. Boug\u00e9, P. Fraigniaud, A. Mignotte, and Y. Robert, editors, Euro-Par'96. Parallel Processing, number 1123--1124 in LNCS, Lyon, August 1996 . LIP-ENSL, Springer . H. Jifeng, Q. Miller, and L. Chen. Algebraic laws for BSP programming. In L. Boug\u00e9, P. Fraigniaud, A. Mignotte, and Y. Robert, editors, Euro-Par'96. Parallel Processing, number 1123--1124 in LNCS, Lyon, August 1996. LIP-ENSL, Springer."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40047-6_46"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/PDP.2010.26"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11428848_132"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146847.1146860"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197356"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480905"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0028-7"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2011.04.005"},{"key":"e_1_3_2_1_25_1","unstructured":"The Coq Development Team. The Coq Proof Assistant. http:\/\/coq.inria.fr.  The Coq Development Team. The Coq Proof Assistant. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/79173.79181"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560647_13"}],"event":{"name":"SAC 2014: Symposium on Applied Computing","location":"Gyeongju Republic of Korea","acronym":"SAC 2014","sponsor":["SIGAPP ACM Special Interest Group on Applied Computing"]},"container-title":["Proceedings of the 29th Annual ACM Symposium on Applied Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2554850.2554912","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2554850.2554912","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:17Z","timestamp":1750234697000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2554850.2554912"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,24]]},"references-count":25,"alternative-id":["10.1145\/2554850.2554912","10.1145\/2554850"],"URL":"https:\/\/doi.org\/10.1145\/2554850.2554912","relation":{},"subject":[],"published":{"date-parts":[[2014,3,24]]},"assertion":[{"value":"2014-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}