{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T08:41:58Z","timestamp":1773736918269,"version":"3.50.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T00:00:00Z","timestamp":1740441600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T00:00:00Z","timestamp":1740441600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Parallel Prog"],"published-print":{"date-parts":[[2025,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for <jats:italic>dependently-typed languages<\/jats:italic>, such as Idris, Agda and Coq. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present , a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in <jats:italic>Pipeline<\/jats:italic> and <jats:italic>Task Farm<\/jats:italic> skeletons. We evaluate  on a series of standard <jats:italic>Task Farm<\/jats:italic> and <jats:italic>Pipeline<\/jats:italic> examples, achieving speedups of up to 23.35<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u00d7<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> on a 28-core machine.<\/jats:p>","DOI":"10.1007\/s10766-025-00794-3","type":"journal-article","created":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T16:23:32Z","timestamp":1740500612000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["pi-par: A Dependently-Typed Parallel Language with Algorithmic Skeletons"],"prefix":"10.1007","volume":"53","author":[{"given":"Christopher","family":"Brown","sequence":"first","affiliation":[]},{"given":"Adam D.","family":"Barwell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,2,25]]},"reference":[{"issue":"10","key":"794_CR1","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1145\/1562764.1562783","volume":"52","author":"K Asanovic","year":"2009","unstructured":"Asanovic, K., Bod\u00edk, R., Demmel, J., Keaveny, T., Keutzer, K., Kubiatowicz, J., Morgan, N., Patterson, D.A., Sen, K., Wawrzynek, J., Wessel, D., Yelick, K.A.: A view of the parallel computing landscape. Commun. ACM 52(10), 56\u201367 (2009)","journal-title":"Commun. ACM"},{"key":"794_CR2","doi-asserted-by":"crossref","unstructured":"Rio\u00a0Astorga, D., Dolz, M.F., Fern\u00e1ndez, J., Garc\u00eda, J.D.: A generic parallel pattern interface for stream and data processing. Concurr. Comput. Pract. Exp. 29(24) (2017)","DOI":"10.1002\/cpe.4175"},{"key":"794_CR3","unstructured":"Robinson, A.D.: TBB (Intel Threading Building Blocks). In: Encyclopedia of Parallel Computing, p. 2029. Springer, Berlin, Heidelberg (2011)"},{"key":"794_CR4","volume-title":"A Parallel Programming with Microsoft Visual C++: Design Patterns for Decomposition and Coordination on Multicore Architectures","author":"C Campbell","year":"2011","unstructured":"Campbell, C., Miller, A.: A Parallel Programming with Microsoft Visual C++: Design Patterns for Decomposition and Coordination on Multicore Architectures, 1st edn. Microsoft Press, USA (2011)","edition":"1"},{"key":"794_CR5","volume-title":"Parallel Programming in OpenMP","author":"R Chandra","year":"2001","unstructured":"Chandra, R.: Parallel Programming in OpenMP. Morgan Kaufmann, USA (2001)"},{"key":"794_CR6","unstructured":"Weirich, S.: Implementing Dependent Types in pi-forall. CoRR https:\/\/arxiv.org\/abs\/2207.02129 (2022)"},{"key":"794_CR7","doi-asserted-by":"publisher","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda\u2014a functional language with dependent types. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics. TPHOLs \u201909, pp. 73\u201378. Springer, Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"794_CR8","unstructured":"Brady, E.: Type-driven Development With Idris. Manning, UK (2016). http:\/\/www.worldcat.org\/isbn\/9781617293023"},{"key":"794_CR9","unstructured":"Dowek, G., Felty, A., Herbelin, H., Huet, G., Parent, C., Paulin-Mohring, C., Werner, B., Murthy, C.: The Coq Proof Assistant User\u2019s Guide: Version 5.8. PhD thesis, INRIA (1993)"},{"key":"794_CR10","doi-asserted-by":"crossref","unstructured":"Brady, E.C.: Type-driven development of concurrent communicating systems. Comput. Sci. 18(3) (2017)","DOI":"10.7494\/csci.2017.18.3.1413"},{"key":"794_CR11","unstructured":"Armstrong, J., Virding, R., Wikstrom, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice Hall PTR, Englewood Cliffs, New Jersey 07632 (1996)"},{"issue":"4","key":"794_CR12","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1007\/s10766-013-0266-5","volume":"42","author":"C Brown","year":"2014","unstructured":"Brown, C., Danelutto, M., Hammond, K., Kilpatrick, P., Elliott, A.: Cost-directed refactoring for parallel Erlang programs. Int. J. Parallel Program. 42(4), 564\u2013582 (2014)","journal-title":"Int. J. Parallel Program."},{"key":"794_CR13","doi-asserted-by":"publisher","unstructured":"Brown, C., Janjic, V., Barwell, A., Garcia, J.D.: Refactoring GrPPI: Generic refactoring for generic parallelism in C++. In: 12th International Symposium on High-Level Parallel Programming and Applications (2019).https:\/\/doi.org\/10.1007\/s10766-020-00667-x . https:\/\/risweb.st-andrews.ac.uk\/portal\/en\/researchoutput\/refactoring-grppi(84dd2979-e2bf-456c-9991-73e3cd996a17).html","DOI":"10.1007\/s10766-020-00667-x"},{"key":"794_CR14","unstructured":"Marlow, S., et al.: Haskell 2010 Language Report. Available online http:\/\/www.haskell.org\/ (May 2011) (2010)"},{"key":"794_CR15","doi-asserted-by":"crossref","unstructured":"Marlow, S.: Parallel and concurrent programming in Haskell. In: CEFP. Lecture Notes in Computer Science, vol. 7241, pp. 339\u2013401. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-32096-5_7"},{"key":"794_CR16","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-45361-X_4","volume-title":"Implementation of Functional Languages","author":"RF Pointon","year":"2001","unstructured":"Pointon, R.F., Trinder, P.W., Loidl, H.-W.: The design and implementation of Glasgow distributed Haskell. In: Mohnen, M., Koopman, P. (eds.) Implementation of Functional Languages, pp. 53\u201370. Springer, Berlin, Heidelberg (2001)"},{"key":"794_CR17","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/10722298_11","volume-title":"Implementation of Functional Languages","author":"K Hammond","year":"2000","unstructured":"Hammond, K., Reb\u00f3n Portillo, \u00c1.J.: HaskSkel: Algorithmic Skeletons in Haskell. In: Koopman, P., Clack, C. (eds.) Implementation of Functional Languages, pp. 181\u2013198. Springer, Berlin, Heidelberg (2000)"},{"issue":"3","key":"794_CR18","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1017\/S0956796805005526","volume":"15","author":"R Loogen","year":"2005","unstructured":"Loogen, R., Ortega-Mall\u00e9n, Y., Pe\u00f1a-Mar\u00ed, R.: Parallel functional programming in Eden. J. Funct. Program. 15(3), 431\u2013475 (2005)","journal-title":"J. Funct. Program."},{"issue":"4","key":"794_CR19","first-page":"792","volume":"35","author":"AD Barwell","year":"2016","unstructured":"Barwell, A.D., Brown, C., Hammond, K., Turek, W., Byrski, A.: Using program shaping and algorithmic skeletons to parallelise an evolutionary multi-agent system in Erlang. Comput. Inform. 35(4), 792\u2013818 (2016)","journal-title":"Comput. Inform."},{"key":"794_CR20","doi-asserted-by":"crossref","unstructured":"Brown, C., Janjic, V., Hammond, K., Sch\u00f6ner, H., Idrees, K., Glass, C.W.: Agricultural reform: more efficient farming using advanced parallel refactoring tools. In: PDP, pp. 36\u201343. IEEE Computer Society, Washington DC, USA (2014)","DOI":"10.1109\/PDP.2014.94"},{"issue":"14","key":"794_CR21","doi-asserted-by":"crossref","first-page":"e5420","DOI":"10.1002\/cpe.5420","volume":"33","author":"V Janjic","year":"2019","unstructured":"Janjic, V., Brown, C., Barwell, A.D., Hammond, K.: Refactoring for introducing and tuning parallelism for heterogeneous multicore machines in Erlang. Concurr. Comput. Pract. Exp. 33(14), e5420 (2019)","journal-title":"Concurr. Comput. Pract. Exp."},{"key":"794_CR22","unstructured":"Janjic, V., Brown, C., Hammond, K.: Lapedo: hybrid skeletons for programming heterogeneous multicore machines in Erlang. In: PARCO. Advances in Parallel Computing, vol. 27, pp. 185\u2013195. IOS Press, Netherlands (2016)"},{"key":"794_CR23","doi-asserted-by":"crossref","unstructured":"Janjic, V., Brown, C., MacKenzie, K., Hammond, K., Danelutto, M., Aldinucci, M., Garc\u00eda, J.D.: RPL: a domain-specific language for designing and implementing parallel C++ applications. In: PDP, pp. 288\u2013295. IEEE Computer Society, Washington DC, USA (2016)","DOI":"10.1109\/PDP.2016.122"},{"issue":"6","key":"794_CR24","doi-asserted-by":"crossref","first-page":"886","DOI":"10.1007\/s10766-021-00716-z","volume":"49","author":"V Janjic","year":"2021","unstructured":"Janjic, V., Brown, C., Barwell, A.D.: Restoration of legacy parallelism: transforming Pthreads into farm and pipeline patterns. Int. J. Parallel Program. 49(6), 886\u2013910 (2021)","journal-title":"Int. J. Parallel Program."},{"key":"794_CR25","volume-title":"Intel Threading Building Blocks: Outfitting C++ for Multi-core Processor Parallelism","author":"J Reinders","year":"2007","unstructured":"Reinders, J.: Intel Threading Building Blocks: Outfitting C++ for Multi-core Processor Parallelism. O\u2019Reilly Media Inc, USA (2007)"},{"key":"794_CR26","doi-asserted-by":"crossref","unstructured":"Aldinucci, M., Danelutto, M., Kilpatrick, P., Torquati, M.: Fastflow: high-level and efficient streaming on multi-core. Programming Multi-Core and Many-Core Computing Systems, Parallel and Distributed Computing (2017)","DOI":"10.1002\/9781119332015.ch13"},{"key":"794_CR27","doi-asserted-by":"crossref","unstructured":"Enmyren, J., Kessler, C.W.: SkePU: a multi-backend skeleton programming library for multi-GPU systems. In: HLPP, pp. 5\u201314. ACM, New York, NY, USA (2010)","DOI":"10.1145\/1863482.1863487"},{"key":"794_CR28","unstructured":"Ciechanowicz, P., Poldner, M., Kuchen, H.: The M\u00fcnster skeleton library muesli: a comprehensive overview. ERCIS Working Papers\u00a07, University of M\u00fcnster, European Research Center for Information Systems (ERCIS) (2009). https:\/\/ideas.repec.org\/p\/zbw\/ercisw\/7.html"},{"key":"794_CR29","unstructured":"Barwell, A.D.: Pattern Discovery for Parallelism in Functional Languages. PhD thesis, University of St Andrews, UK (2018)"},{"key":"794_CR30","doi-asserted-by":"crossref","unstructured":"Castro, D., Hammond, K., Sarkar, S.: Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms. In: ICFP, pp. 4\u201317. ACM, Washington DC, USA (2016)","DOI":"10.1145\/2951913.2951920"},{"key":"794_CR31","doi-asserted-by":"crossref","unstructured":"Honda, K.: Types for dyadic interaction. In: CONCUR. Lecture Notes in Computer Science, vol. 715, pp. 509\u2013523. Springer, Berlin, Heidelberg (1993)","DOI":"10.1007\/3-540-57208-2_35"},{"key":"794_CR32","doi-asserted-by":"crossref","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. Lecture Notes in Computer Science, vol. 1381, pp. 122\u2013138. Springer, Berlin, Heidelberg (1998)","DOI":"10.1007\/BFb0053567"},{"issue":"1","key":"794_CR33","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/2827695","volume":"63","author":"K Honda","year":"2016","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9\u20131967 (2016)","journal-title":"J. ACM"},{"key":"794_CR34","doi-asserted-by":"crossref","unstructured":"Yoshida, N., Gheri, L.: A very gentle introduction to multiparty session types. In: ICDCIT. Lecture Notes in Computer Science, vol. 11969, pp. 73\u201393. Springer, Cham, Switzerland (2020)","DOI":"10.1007\/978-3-030-36987-3_5"},{"issue":"POPL","key":"794_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3290342","volume":"3","author":"D Castro-Perez","year":"2019","unstructured":"Castro-Perez, D., Hu, R., Jongmans, S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang. 3(POPL), 1\u201310 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"794_CR36","doi-asserted-by":"crossref","unstructured":"Cutner, Z., Yoshida, N., Vassor, M.: Deadlock-free asynchronous message reordering in rust with multiparty session types. In: PPoPP, pp. 246\u2013261. ACM, New York, USA (2022)","DOI":"10.1145\/3503221.3508404"},{"key":"794_CR37","unstructured":"Barwell, A.D., Hou, P., Yoshida, N., Zhou, F.: Designing asynchronous multiparty protocols with crash-stop failures. In: ECOOP. LIPIcs, vol. 263, pp. 1\u20131130. Schloss Dagstuhl\u2013Leibniz\u2013Zentrum f\u00fcr Informatik, Germany (2023)"},{"issue":"OOPSLA","key":"794_CR38","first-page":"148","volume":"4","author":"F Zhou","year":"2020","unstructured":"Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148\u2013114830 (2020)","journal-title":"Proc. ACM Program. Lang."},{"issue":"OOPSLA1","key":"794_CR39","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1145\/3586031","volume":"7","author":"L Gheri","year":"2023","unstructured":"Gheri, L., Yoshida, N.: Hybrid multiparty session types: compositionality for protocol specification through endpoint projection. Proc. ACM Program. Lang. 7(OOPSLA1), 112\u2013142 (2023)","journal-title":"Proc. ACM Program. Lang."},{"issue":"2","key":"794_CR40","doi-asserted-by":"publisher","first-page":"10","DOI":"10.4230\/DARTS.9.2.10","volume":"9","author":"D Castro-Perez","year":"2023","unstructured":"Castro-Perez, D., Yoshida, N.: Dynamically updatable multiparty session protocols (Artifact). Dagstuhl Artifacts Ser. 9(2), 10\u20131102 (2023). https:\/\/doi.org\/10.4230\/DARTS.9.2.10","journal-title":"Dagstuhl Artifacts Ser."},{"key":"794_CR41","unstructured":"Barwell, A.D., Scalas, A., Yoshida, N., Zhou, F.: Generalised multiparty session types with crash-stop failures. In: CONCUR. LIPIcs, vol. 243, pp. 35\u201313525. Schloss Dagstuhl\u2013Leibniz\u2013Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022)"},{"issue":"ICFP","key":"794_CR42","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1145\/3607832","volume":"7","author":"S Fowler","year":"2023","unstructured":"Fowler, S., Attard, D.P., Sowul, F., Gay, S.J., Trinder, P.: Special Delivery: Programming with Mailbox Types. Proc. ACM Program. Lang. 7(ICFP), 78\u2013107 (2023)","journal-title":"Proc. ACM Program. Lang."}],"container-title":["International Journal of Parallel Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-025-00794-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10766-025-00794-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10766-025-00794-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T22:02:53Z","timestamp":1743890573000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10766-025-00794-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,25]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["794"],"URL":"https:\/\/doi.org\/10.1007\/s10766-025-00794-3","relation":{},"ISSN":["0885-7458","1573-7640"],"issn-type":[{"value":"0885-7458","type":"print"},{"value":"1573-7640","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,2,25]]},"assertion":[{"value":"30 September 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"11"}}