{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T04:24:30Z","timestamp":1744086270935,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642330773"},{"type":"electronic","value":"9783642330780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33078-0_16","type":"book-chapter","created":{"date-parts":[[2012,9,3]],"date-time":"2012-09-03T21:37:49Z","timestamp":1346708269000},"page":"218-232","source":"Crossref","is-referenced-by-count":2,"title":["A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays"],"prefix":"10.1007","author":[{"given":"Wadoud","family":"Bousdira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Loulergue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Tesson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3-4","key":"16_CR1","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/j.cl.2006.07.004","volume":"33","author":"M. Aldinucci","year":"2007","unstructured":"Aldinucci, M., Danelutto, M.: Skeleton-based parallel programming: Functional and parallel semantics in a single shot. Computer Languages, Systems and Structures\u00a033(3-4), 179\u2013192 (2007)","journal-title":"Computer Languages, Systems and Structures"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Bentley, J.: Programming Pearls. Addison-Wesley (1986)","DOI":"10.1145\/6424.315691"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Caromel, D., Henrio, L., Leyton, M.: Type safe algorithmic skeletons. In: EuroMicro PDP, pp. 45\u201353. IEEE Computer Society (2008)","DOI":"10.1109\/PDP.2008.29"},{"key":"16_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, pp. 804\u2013812. ACM (2000)","DOI":"10.1145\/338407.338568"},{"key":"16_CR5","unstructured":"Cole, M.: Algorithmic Skeletons: Structured Management of Parallel Computation. MIT Press (1989), http:\/\/homepages.inf.ed.ac.uk\/mic\/Pubs"},{"key":"16_CR6","unstructured":"Cole, M.: Parallel Programming, List Homomorphisms and the Maximum Segment Sum Problem. In: Joubert, G.R., Trystram, D., Peters, F.J., Evans, D.J. (eds.) ParCo 1993, pp. 489\u2013492. Elsevier (1994)"},{"issue":"3-4","key":"16_CR7","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.cl.2006.07.005","volume":"33","author":"R. Cosmo Di","year":"2007","unstructured":"Di Cosmo, R., Pelagatti, S., Li, Z.: A calculus for parallel computations over multidimensional dense arrays. Computer Language Structures and Systems\u00a033(3-4), 82\u2013110 (2007)","journal-title":"Computer Language Structures and Systems"},{"key":"16_CR8","unstructured":"Falcou, J., S\u00e9rot, J.: Formal Semantics Applied to the Implementation of a Skeleton-Based Parallel Programming Library. In: Bischof, C.H., B\u00fccker, H.M., Gibbon, P., Joubert, G.R., Lippert, T., Mohr, B., Peters, F.J. (eds.) ParCo 2007, pp. 243\u2013252. IOS Press (2007)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Gesbert, L., Hu, Z., Loulergue, F., Matsuzaki, K., Tesson, J.: Systematic Development of Correct BSP Programs. In: PDCAT, pp. 334\u2013340. IEEE (2010)","DOI":"10.1109\/PDCAT.2010.86"},{"issue":"12","key":"16_CR10","doi-asserted-by":"publisher","first-page":"1135","DOI":"10.1002\/spe.1026","volume":"40","author":"H. Gonz\u00e1lez-V\u00e9lez","year":"2010","unstructured":"Gonz\u00e1lez-V\u00e9lez, H., Leyton, M.: A survey of algorithmic skeleton frameworks: high-level structured parallel programming enablers. Software, Practrice & Experience\u00a040(12), 1135\u20131160 (2010)","journal-title":"Software, Practrice & Experience"},{"issue":"1","key":"16_CR11","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/963778.963780","volume":"26","author":"S. Gorlatch","year":"2004","unstructured":"Gorlatch, S.: Send-receive considered harmful: Myths and realities of message passing. ACM TOPLAS\u00a026(1), 47\u201356 (2004)","journal-title":"ACM TOPLAS"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1142\/S0129626402000938","volume":"12","author":"M. Hidalgo-Herrero","year":"2002","unstructured":"Hidalgo-Herrero, M., Ortega-Mall\u00e9n, Y.: An Operational Semantics for the Parallel Language Eden. Parallel Processing Letters\u00a012(2), 211\u2013228 (2002)","journal-title":"Parallel Processing Letters"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Hutton, G.: Programming in Haskell. Cambridge University Press (2007)","DOI":"10.1017\/CBO9780511813672"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-23178-0_4","volume-title":"Parallel Computing Technologies","author":"N. Javed","year":"2011","unstructured":"Javed, N., Loulergue, F.: A Formal Programming Model of Orl\u00e9ans Skeleton Library. In: Malyshkin, V. (ed.) PaCT 2011. LNCS, vol.\u00a06873, pp. 40\u201352. Springer, Heidelberg (2011)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Javed, N., Loulergue, F.: Parallel Programming and Performance Predictability with Orl\u00e9ans Skeleton Library. In: HPCS, pp. 257\u2013263. IEEE (2011)","DOI":"10.1109\/HPCSim.2011.5999832"},{"key":"16_CR16","unstructured":"Javed, N., Loulergue, F., Tesson, J., Bousdira, W.: Prototyping a Library of Algorithmic Skeletons with BSML. In: PDPTA 2011, pp. 520\u2013526. CSREA Press (2011)"},{"key":"16_CR17","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml System release 3.12 (2010), http:\/\/caml.inria.fr"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An Overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"issue":"15","key":"16_CR19","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1017\/S0956796805005526","volume":"3","author":"R. Loogen","year":"2005","unstructured":"Loogen, R., Ortega-Mallen, Y., Pena-Mari, R.: Parallel functional programming in eden. Journal of Functional Programming\u00a03(15), 431\u2013475 (2005)","journal-title":"Journal of Functional Programming"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1046","DOI":"10.1007\/11428848_132","volume-title":"Computational Science \u2013 ICCS 2005","author":"F. Loulergue","year":"2005","unstructured":"Loulergue, F., Gava, F., Billiet, D.: Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. In: Sunderam, V.S., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds.) ICCS 2005. LNCS, vol.\u00a03515, pp. 1046\u20131054. Springer, Heidelberg (2005)"},{"key":"16_CR21","unstructured":"Loulergue, F., Tesson, J., Bousdira, W.: Certified BSML and Verified OSL Prototype version 0.3 (April 2012), http:\/\/traclifo.univ-orleans.fr\/BSML"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Matsuzaki, K., Iwasaki, H., Emoto, K., Hu, Z.: A Library of Constructive Skeletons for Sequential Style of Parallel Programming. In: InfoScale 2006. ACM Press (2006)","DOI":"10.1145\/1146847.1146860"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Tesson, J., Loulergue, F.: A Verified BSML Heat Diffusion Simulation. In: ICCS. Procedia Computer Science, pp. 36\u201345. Elsevier (2011)","DOI":"10.1016\/j.procs.2011.04.005"},{"key":"16_CR24","unstructured":"The Coq Development Team: The Coq Proof Assistant, http:\/\/coq.inria.fr"},{"issue":"8","key":"16_CR25","doi-asserted-by":"crossref","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. CACM\u00a033(8), 103 (1990)","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Architectures for Parallel Processing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33078-0_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T19:54:36Z","timestamp":1744055676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33078-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642330773","9783642330780"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33078-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}