{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:51:49Z","timestamp":1725796309342},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319089690"},{"type":"electronic","value":"9783319089706"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_17","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:13:26Z","timestamp":1403954006000},"page":"258-274","source":"Crossref","is-referenced-by-count":7,"title":["A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction"],"prefix":"10.1007","author":[{"given":"Kento","family":"Emoto","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Tesson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Cole, M.: Algorithmic Skeletons: Structured Management of Parallel Computation. MIT Press (1989), \n \n http:\/\/homepages.inf.ed.ac.uk\/mic\/Pubs"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jda.2013.03.003","volume":"21","author":"R.C. Corra","year":"2013","unstructured":"Corra, R.C., Farias, P.M., de Souza, C.P.: Insertion and sorting in a sequence of numbers minimizing the maximum sum of a contiguous subsequence. Journal of Discrete Algorithms\u00a021, 1\u201310 (2013)","journal-title":"Journal of Discrete Algorithms"},{"issue":"4-6","key":"17_CR3","doi-asserted-by":"publisher","first-page":"623","DOI":"10.1007\/s00165-012-0241-8","volume":"24","author":"K. Emoto","year":"2012","unstructured":"Emoto, K., Fischer, S., Hu, Z.: Filter-embedding semiring fusion for programming with MapReduce. Formal Aspects of Computing\u00a024(4-6), 623\u2013645 (2012)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-28869-2_13","volume-title":"Programming Languages and Systems","author":"K. Emoto","year":"2012","unstructured":"Emoto, K., Fischer, S., Hu, Z.: Generate, Test, and Aggregate \u2013 A Calculation-based Framework for Systematic Parallel Programming with MapReduce. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 254\u2013273. Springer, Heidelberg (2012)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-38613-8_9","volume-title":"Integrated Formal Methods","author":"F. Gava","year":"2013","unstructured":"Gava, F., Fortin, J., Guedj, M.: Deductive Verification of State-Space Algorithms. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 124\u2013138. Springer, Heidelberg (2013)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Gesbert, L., Hu, Z., Loulergue, F., Matsuzaki, K., Tesson, J.: Systematic Development of Correct Bulk Synchronous Parallel Programs. In: International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), pp. 334\u2013340. IEEE (2010)","DOI":"10.1109\/PDCAT.2010.86"},{"issue":"2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1109\/TSP.2005.861753","volume":"54","author":"T.J. Ho","year":"2006","unstructured":"Ho, T.J., Chen, B.S.: Novel extended viterbi-based multiple-model algorithms for state estimation of discrete-time systems with markov jump parameters. IEEE Transactions on Signal Processing\u00a054(2), 393\u2013404 (2006)","journal-title":"IEEE Transactions on Signal Processing"},{"issue":"1-3","key":"17_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0167-6423(99)00029-5","volume":"37","author":"F. Loulergue","year":"2000","unstructured":"Loulergue, F., Hains, G., Foisy, C.: A Calculus of Functional BSP Programs. Science of Computer Programming\u00a037(1-3), 253\u2013277 (2000)","journal-title":"Science of Computer Programming"},{"key":"17_CR9","unstructured":"Lupinski, N., Falcou, J., Paulin-Mohring, C.: S\u00e9mantique d\u2019une langage de squelettes (2012), \n \n http:\/\/www.lri.fr\/~paulin\/Skel\/article.pdf"},{"issue":"2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.jsc.2010.08.004","volume":"46","author":"G. Malecha","year":"2011","unstructured":"Malecha, G., Morrisett, G., Wisnesky, R.: Trace-based verification of imperative programs with i\/o. J. Symb. Comput.\u00a046(2), 95\u2013118 (2011)","journal-title":"J. Symb. Comput."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70594-9_15","volume-title":"Mathematics of Program Construction","author":"S.-C. Mu","year":"2008","unstructured":"Mu, S.-C., Ko, H.-S., Jansson, P.: Algebra of programming using dependent types. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 268\u2013283. Springer, Heidelberg (2008)"},{"issue":"3","key":"17_CR12","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/j.jsc.2003.07.002","volume":"37","author":"F. Otto","year":"2004","unstructured":"Otto, F., Sokratova, O.: Reduction relations for monoid semirings. Journal of Symbolic Computation\u00a037(3), 343\u2013376 (2004)","journal-title":"Journal of Symbolic Computation"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Snir, M., Gropp, W.: MPI the Complete Reference. MIT Press (1998)","DOI":"10.7551\/mitpress\/4789.001.0001"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/s10990-011-9075-y","volume":"23","author":"W. Swierstra","year":"2010","unstructured":"Swierstra, W.: More dependent types for distributed arrays. Higher-Order and Symbolic Computation\u00a023(4), 489\u2013506 (2010)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"17_CR15","unstructured":"SyDPaCC Home Page, \n \n http:\/\/traclifo.univ-orleans.fr\/SyDPaCC"},{"issue":"8","key":"17_CR16","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/79173.79181","volume":"33","author":"L.G. Valiant","year":"1990","unstructured":"Valiant, L.G.: A bridging model for parallel computation. Commun. ACM\u00a033(8), 103 (1990)","journal-title":"Commun. ACM"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM (1989)","DOI":"10.1145\/99370.99404"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/11560647_13","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"J. Zhou","year":"2005","unstructured":"Zhou, J., Chen, Y.: Generating C code from LOGS specifications. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 195\u2013210. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08970-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:39:09Z","timestamp":1558319949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}