As some of you may have seen from our recent PostDoc recruitment announcement, Koen Claessen, Mary Sheeran, and I are looking for new researchers to join the FP group at Chalmers. While Koen is driving a track focused on language foundations and semantics (funded by Epic Games), I want to take a moment here to expand on my and Mary's part of the puzzle: the FunPACT project.
About FunPACT
FunPACT is a research project exploring the mathematical and programming foundations of multidimensional arrays (tensors).
Our work bridges the gap between ad hoc array processing and formally verified functional programming. Specifically, we focus on formalizing an algebra of array combinators and finite permutations using interactive theorem provers (such as Lean and Agda), exploring how these mathematical structures can be augmented by AI-assisted proof techniques.
This work is funded by the Swedish Research Council (Vetenskapsrådet) under the project title "An Algebra of Array Combinators and its Applications" (grant diary number 2021-05491). The grant was originally awarded to and led by Mary Sheeran, who laid the groundwork for this research. After Mary became professor emerita, the project was formally transferred to me as the Principal Investigator in June 2026. Mary remains part of the team, and we are currently hiring a PostDoc to help us push these ideas further.
Research objectives
We will collect our ongoing research, code, and formal proofs in a FunPACT repository. We are tackling the computational curse of dimensionality by focusing on three main areas:
Domain-Specific Tensor Languages : Developing Embedded DSLs to express tensor access patterns, structured index arithmetic, and partitioning safely and expressively.
Formal Verification : Constructing rigorous proofs of functional correctness for hardware datapaths, algorithm transformations, and array access patterns.
Algebraic Permutations : Formalizing finite permutations and leveraging Vector of Index Bits (VIB) arithmetic to simplify how complex multidimensional array operations are expressed and verified.
Related publications & talks
This project builds on several years of investigation into array combinators and dependent types. For those interested in the technical background, here are a few key publications from the team:
- M. Bouverot-Dupuis, M. Sheeran. A Efficient GPU Implementation of Affine Index Permutations on Arrays. <doi:10.1145/3609024.3609411> (pdf)
- J-P. Bernardy, P. Jansson (2025). Domain-Specific Tensor Languages. Journal of Functional Programming. JFP, (arXiv <doi:10.48550/arXiv.2312.02664>)
- P. Jansson, W. Swierstra (2025). Finite permutations in Agda (WG 2.1 #83). slides (paper forthcoming)
Connecting the dots (earlier blog posts)
If you have been following this blog, the themes in FunPACT will look familiar. This project serves as a natural convergence point for several topics I have written about previously:
- Grant proposal: Navigating the Incomparable: A Functional Programming Approach to Multi-Objective Optimization -- A recent grant proposal which, if funded, will complement the FunPACT project.
- Talk: Domain-specific tensor languages (Oct 2025) & (Dec 2023) -- Background on our JFP paper detailing a two-DSL approach to tensor calculus (using linear types and symmetric monoidal categories).
- Agda-ventures with PolyP (Oct 2025) -- Exploring generic programming in a dependently typed setting, which still influences how we formalize algebraic structures today.
- Dimensional Analysis meets Dependent Types (Dec 2025) -- While physically motivated, this work on the covariance principle shares the same core ambition as FunPACT: using the type checker to guarantee mathematical correctness by construction.
If you find the intersection of functional programming, formal methods, and algebraic structures exciting, please take a look at our open PostDoc position (mastodon post) or get in touch!