{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:41:40Z","timestamp":1770835300275,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T00:00:00Z","timestamp":1459987200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche (FR)","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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Parallel Prog"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s10766-016-0415-8","type":"journal-article","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T05:14:07Z","timestamp":1460006047000},"page":"300-319","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Calculating Parallel Programs in Coq Using List Homomorphisms"],"prefix":"10.1007","volume":"45","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wadoud","family":"Bousdira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Tesson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,7]]},"reference":[{"issue":"3\u20134","key":"415_CR1","first-page":"179","volume":"33","author":"M Aldinucci","year":"2007","unstructured":"Aldinucci, M., Danelutto, M.: Skeleton-based parallel programming: functional and parallel semantics in a single shot. Comput. Lang. Syst. Str. 33(3\u20134), 179\u2013192 (2007)","journal-title":"Comput. Lang. Syst. Str."},{"key":"415_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61455-2_12","volume-title":"Algebra of Programming","author":"R Bird","year":"1996","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall, New Jersey (1996)"},{"key":"415_CR3","doi-asserted-by":"crossref","unstructured":"Bousdira, W., Loulergue, F., Tesson, J.: A verified library of algorithmic skeletons on evenly distributed arrays. In: Algorithms and Architectures for Parallel Processing (ICA3PP). pp. 218\u2013232. No. 7439 in LNCS, Springer, Fukuoka, Japan (2012)","DOI":"10.1007\/978-3-642-33078-0_16"},{"key":"415_CR4","doi-asserted-by":"crossref","unstructured":"Cavarra, A., Riccobene, E., Zavanella, A.: A formal model for the parallel semantics of P3L. In: ACM Symposium on Applied Computing (SAC). pp. 804\u2013812. ACM (2000)","DOI":"10.1145\/338407.338568"},{"issue":"2","key":"415_CR5","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1142\/S0129626495000175","volume":"5","author":"M Cole","year":"1995","unstructured":"Cole, M.: Parallel programming with list homomorphisms. Parallel Process. Lett. 5(2), 191\u2013203 (1995)","journal-title":"Parallel Process. Lett."},{"key":"415_CR6","unstructured":"Daum, M.: Reasoning on data-parallel programs in Isabelle\/Hol. In: C\/C++ Verification Workshop (2007)"},{"key":"415_CR7","doi-asserted-by":"crossref","unstructured":"Emoto, K., Loulergue, F., Tesson, J.: A verified generate-test-aggregate Coq library for parallel programs extraction. In: Interactive Theorem Proving (ITP). pp. 258\u2013274. No. 8558 in LNCS, Springer, Wien (2014)","DOI":"10.1007\/978-3-319-08970-6_17"},{"key":"415_CR8","doi-asserted-by":"publisher","unstructured":"Fortin, J., Gava, F.: BSP-Why: a tool for deductive verification of BSP algorithms with subgroup synchronisation. Int. J. Parallel Prog. (2015). doi: 10.1007\/s10766-015-0360-y","DOI":"10.1007\/s10766-015-0360-y"},{"issue":"3","key":"415_CR9","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1142\/S0129626403001343","volume":"13","author":"F Gava","year":"2003","unstructured":"Gava, F.: Formal proofs of functional BSP programs. Parallel Process. Lett. 13(3), 365\u2013376 (2003)","journal-title":"Parallel Process. Lett."},{"key":"415_CR10","doi-asserted-by":"crossref","unstructured":"Gava, F., Gesbert, L., Loulergue, F.: Type system for a safe execution of parallel programs in BSML. In: 5th ACM SIGPLAN Workshop on High-Level Parallel Programming and Applications, pp. 27\u201334. ACM (2011)","DOI":"10.1145\/2034751.2034759"},{"issue":"4","key":"415_CR11","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1017\/S0956796800001908","volume":"6","author":"J Gibbons","year":"1996","unstructured":"Gibbons, J.: The third homomorphism theorem. J. Funct. Program. 6(4), 657\u2013665 (1996)","journal-title":"J. Funct. Program."},{"issue":"7","key":"415_CR12","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"415_CR13","doi-asserted-by":"crossref","unstructured":"Loulergue, F., Gava, F., Billiet, D.: Bulk synchronous parallel ML: modular implementation and performance prediction. In: International Conference on Computational Science (ICCS). LNCS, vol. 3515, pp. 1046\u20131054. Springer, Berlin (2005)","DOI":"10.1007\/11428848_132"},{"key":"415_CR14","doi-asserted-by":"crossref","unstructured":"Loulergue, F., Robillard, S., Tesson, J., L\u00e9gaux, J., Hu, Z.: Formal derivation and extraction of a parallel program for the all nearest smaller values problem. In: ACM Symposium on Applied Computing (SAC). pp. 1577\u20131584. ACM, Gyeongju (2014)","DOI":"10.1145\/2554850.2554912"},{"key":"415_CR15","unstructured":"Lupinski, N., Falcou, J., Paulin-Mohring, C.: S\u00e9mantique d\u2019une langage de squelettes. http:\/\/www.lri.fr\/~paulin\/Skel\/article (2012)"},{"issue":"2","key":"415_CR16","doi-asserted-by":"crossref","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. 46(2), 95\u2013118 (2011)","journal-title":"J. Symb. Comput."},{"key":"415_CR17","first-page":"268","volume-title":"Mathematics of Program Construction, LNCS","author":"SC 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.) Mathematics of Program Construction, LNCS, vol. 5133, pp. 268\u2013283. Springer, Berlin (2008)"},{"issue":"5","key":"415_CR18","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1017\/S0956796809007345","volume":"19","author":"S Mu","year":"2009","unstructured":"Mu, S., Ko, H., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545\u2013579 (2009)","journal-title":"J. Funct. Program."},{"issue":"1","key":"415_CR19","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1007\/s00165-004-0028-7","volume":"16","author":"A Stewart","year":"2004","unstructured":"Stewart, A., Clint, M., Gabarr\u00f3, J.: Barrier synchronisation: axiomatisation and relaxation. Form. Asp. Comput. 16(1), 36\u201350 (2004)","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"415_CR20","doi-asserted-by":"crossref","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. High. Order Symb. Comput. 23(4), 489\u2013506 (2010)","journal-title":"High. Order Symb. Comput."},{"key":"415_CR21","doi-asserted-by":"crossref","unstructured":"Tesson, J., Loulergue, F.: A verified bulk synchronous parallel ML heat diffusion simulation. In: International Conference on Computational Science (ICCS). pp. 36\u201345. Elsevier, Singapore (2011)","DOI":"10.1016\/j.procs.2011.04.005"},{"key":"415_CR22","unstructured":"The Coq Development Team: The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"issue":"8","key":"415_CR23","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1145\/79173.79181","volume":"33","author":"LG Valiant","year":"1990","unstructured":"Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103 (1990)","journal-title":"Commun. ACM"},{"key":"415_CR24","first-page":"133","volume-title":"Theorem Proving in Higher Order Logics, LNCS","author":"M Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol. 3223, pp. 133\u2013142. Springer, Berlin (2004)"},{"key":"415_CR25","unstructured":"Yokoyama, T., Hu, Z., Takeichi, M.: Yicho: a system for programming program calculations. Technical Report METR 2002\u201307, Department of Mathematical Engineering, University of Tokyo (Jun 2002)"},{"key":"415_CR26","doi-asserted-by":"crossref","unstructured":"Zhou, J., Chen, Y.: Generating C code from LOGS specifications. In: 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC\u201905). pp. 195\u2013210. No. 3407 in LNCS, Springer, Berlin (2005)","DOI":"10.1007\/11560647_13"}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-016-0415-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10766-016-0415-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-016-0415-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-016-0415-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T20:02:34Z","timestamp":1559246554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10766-016-0415-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,7]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["415"],"URL":"https:\/\/doi.org\/10.1007\/s10766-016-0415-8","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"value":"0885-7458","type":"print"},{"value":"1573-7640","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,7]]}}}