pi-par: a dependently-typed parallel language with algorithmic skeletons

Christopher Brown; Adam D. Barwell

doi:10.1007/s10766-025-00794-3

pi-par: a dependently-typed parallel language with algorithmic skeletons

Christopher Brown^*, Adam D. Barwell

^*Corresponding author for this work

School of Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 dependently-typed languages, 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 pi-par, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 × on a 28-core machine.

Original language	English
Article number	11
Number of pages	23
Journal	International Journal of Parallel Programming
Volume	53
Issue number	2
Early online date	25 Feb 2025
DOIs	https://doi.org/10.1007/s10766-025-00794-3
Publication status	E-pub ahead of print - 25 Feb 2025

Keywords

Dependent types
Idris
Parallelism
Concurrency
Skeletons
Farm
Pipeline
Erlang

Access to Document

10.1007/s10766-025-00794-3Licence: CC BY

Brown_2025_IJoPP_pi-par-dependently-typed-parallel-language_CC
© 2025 The Author(s). This article is licensed under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Final published version, 1.25 MBLicence: CC BY

Cite this

@article{e523ed902c2a41b5ad71410611d32fa2,

title = "pi-par: a dependently-typed parallel language with algorithmic skeletons",

abstract = "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 dependently-typed languages, 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 pi-par, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 × on a 28-core machine.",

keywords = "Dependent types, Idris, Parallelism, Concurrency, Skeletons, Farm, Pipeline, Erlang",

author = "Christopher Brown and Barwell, {Adam D.}",

year = "2025",

month = feb,

day = "25",

doi = "10.1007/s10766-025-00794-3",

language = "English",

volume = "53",

journal = "International Journal of Parallel Programming",

issn = "0885-7458",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - pi-par

T2 - a dependently-typed parallel language with algorithmic skeletons

AU - Brown, Christopher

AU - Barwell, Adam D.

PY - 2025/2/25

Y1 - 2025/2/25

N2 - 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 dependently-typed languages, 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 pi-par, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 × on a 28-core machine.

AB - 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 dependently-typed languages, 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 pi-par, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 × on a 28-core machine.

KW - Dependent types

KW - Idris

KW - Parallelism

KW - Concurrency

KW - Skeletons

KW - Farm

KW - Pipeline

KW - Erlang

U2 - 10.1007/s10766-025-00794-3

DO - 10.1007/s10766-025-00794-3

M3 - Article

SN - 0885-7458

VL - 53

JO - International Journal of Parallel Programming

JF - International Journal of Parallel Programming

IS - 2

M1 - 11

ER -

pi-par: a dependently-typed parallel language with algorithmic skeletons

Abstract

Keywords

Access to Document

Fingerprint

Cite this