Pith. sign in

REVIEW 3 major objections 6 minor 73 references

Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language

T0 review · 3 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that a fixed set of array properties — range, monotonicity, injectivity, bijectivity, and filtering/partitioning — can be automatically verified in a purely functional data-parallel language by representing every array as…

desk verdict Real new technique and honest evaluation, but the query solver's UnBef rewrite has an off-by-one unsoundness that currently breaks the verified-implies-true claim. read the letter →

arxiv 2506.23058 v1 pith:7RZUTTNJ submitted 2025-06-29 cs.PL cs.DC

Nikolaj Hey Hinnerskov , Robert Schenck , Cosmin E. Oancea This is my paper · ORCID
classification cs.PLcs.DC
keywords indexfunctionsarraypropertiesFourier-Motzkinverificationdata-parallelFutharkscattersafetyinjectivity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper builds a compiler analysis that lets a purely functional data-parallel language prove facts about the arrays it creates: that an array's values lie in a given range, that they are monotonically ordered, that no value repeats, that a scatter writes to distinct locations, and that a flat array is a filtered, partitioned copy of another. The central trick is to give every array an index function — a case-split expression saying what value lives at each position — and then to reduce each property to algebraic (in)equalities that a Fourier-Motzkin-based solver checks. If the proof succeeds, the compiler can drop runtime bounds checks and scatter-safety checks, which the paper shows speeds up GPU programs by 4 to 12.8 times while keeping average verification time around one second. The intended payoff is that ordinary programmer-written pre- and postconditions replace hand-written proofs.

What carries the argument

Index functions are the central object: an array is represented not as a memory buffer but as a named iterator domain followed by a finite set of guarded expressions (polynomials by cases) that give the value at each index, together with a special ∞ symbol marking filtered-out points and segmented domains that express jagged arrays with empty segments. The property manager turns each wanted property into a set of sufficient-condition queries, and the query solver answers those queries by simplification plus a custom Fourier-Motzkin elimination whose symbol tables record ranges, equivalences, injectivity, and monotonicity. The rewrite system for sums of array slices is what makes the solver practical: it extends slices with known-equivalent boundary elements, merges contiguous slices, cancels overlapping subtracted slices, and peels indices with tighter ranges, so that queries like the partition2 inequality collapse to trivial constants.

What would settle it

Take a program with a deliberately unsafe scatter — an index array with a duplicate in-bounds value whose guard structure makes the duplicate hard to spot — and run the pass: if the system reports the scatter safe, a simplification or elimination step is unsound. A stronger version is to instrument the solver to dump each rewrite and the final eliminated subproblems, then verify those steps against an independent arithmetic evaluator on random small inputs.

Watch

Extended reading notes

Core claim

The paper's central claim is that a small set of array properties — range, monotonicity, injectivity, bijectivity, and filtering/partitioning — can be automatically verified and propagated for non-linear indexing programs by representing every array as an index function, a guarded expression over a (possibly segmented) iteration domain, and discharging each property to a query solver that adapts Fourier-Motzkin elimination to terms built from array indexing and sums of array slices. The framework deliberately does not chase decidability or arbitrary user-defined properties; instead it chooses this fixed property vocabulary because it is easy to annotate, exposes a compositional algebra for inference, and covers the checks that actually appear in data-parallel code: safe scatter (no duplicate in-bounds indices), in-bounds indexing, and filter/partition postconditions. On seven applications, all indexing and scatter operations are verified statically, with an average check time of about one second.

Load-bearing premise

The whole proof chain depends on the solver's algebraic simplification and Fourier-Motzkin adaptation being semantics-preserving: if the rewrites ever turn an unsatisfiable inequality into one that appears satisfiable, then a checked property can be false at runtime.

Editorial extensions

If this is right

  • Programmers annotate only pre- and postconditions; injectivity, bijectivity, and filter/partition postconditions are then verified fully automatically for flat and segmented code, including code built from scan and scatter.
  • Verified scatter safety and verified in-bounds indexing let the CUDA backend remove dynamic checks and skip initializing the destination array, giving 4–12.8x speedups on partition2 at 50–200 million elements.
  • The analysis scales to graph and sparse kernels: maxMatching's histogram-based uniqueness postcondition is proved from the injectivity of the edge index array in about 0.7 seconds, and sparse k-means bounds checks are eliminated with an average 2x speedup.
  • Because properties are a fixed, documented set, the compiler can also infer properties at a high level without an index function — for example, filtering an injective array stays injective — which keeps most checks under one second.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same machinery could plausibly verify other properties that reduce to algebraic constraints on index functions, such as per-segment sortedness or absence of data races in a composed scatter-gather pair, without changing the solver.
  • A natural testable extension is to feed the solver's proof obligations to an independent verified arithmetic checker so that the risk posed by handwritten rewrite rules is contained, since the paper stakes correctness on those rewrites.
  • The property vocabulary might generalize to user-defined predicates that are still algebraic — for example piecewise-linear predicates — giving domain experts more expressive postconditions while keeping the Fourier-Motzkin discharging argument intact.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper presents a framework for automatically verifying properties of integral index arrays in the purely functional data-parallel language Futhark. Arrays are represented as index functions, and the system infers and verifies properties such as range, monotonicity, injectivity, bijectivity, and filtering/partitioning by translating them into algebraic (in)equalities that are discharged by a Fourier-Motzkin-based query solver with a custom simplification engine for sums of array slices. The evaluation reports successful verification of seven benchmarks, with an average verification time around one second, and GPU speedups of up to 12.8x when dynamic bounds checks are eliminated.

Significance. If sound, this is a valuable contribution: it targets non-linear indexing through gather, scatter, and scan, which is beyond the reach of existing linear array logics, and it integrates verification with compiler optimizations in a purely functional data-parallel setting. The design is compositional, with a high-level property algebra that reuses previously proved properties, and the evaluation demonstrates practical verification times and clear performance benefits. The paper ships no machine-checked proofs, and the soundness of the query solver rests on informal arguments about the simplification rules, so the correctness of the central claim depends on those rules being semantics-preserving.

major comments (3)
  1. [§5.3, Fig. 15 (rule B4)] The rule B4 is not semantics-preserving as written. For k1 = -k2, t1 = t2, X = Y, and pb_x ≤ pb_y ≤ pe_y ≤ pe_x, the original two terms equal k1·t1·(s1 - s2) = k1·t1·(s'1 + s'2), where s'1 = ÍX[pb_x:pb_y-1] and s'2 = ÍX[pe_y+1:pe_x]. The rule concludes k1·s'1·t1 + k2·s'2·t2 = k1·t1·(s'1 - s'2), which is different unless s'2 is zero. Concretely, with X[i]=1 for all i, pb_x=0, pe_x=4, pb_y=1, pe_y=3, k1=1, k2=-1, and t1=t2=1, the left-hand side evaluates to 5-3=2 and the right-hand side evaluates to 1-1=0. Because Algorithm 2 (SimplifyΔ) applies B4 to a fix point, this unsound rewrite can be used inside Fourier-Motzkin elimination (Algorithm 1) and can lead the solver to prove a false inequality, undermining the central claim that a successful proof implies the property holds.
  2. [§5.3, Fig. 15 (rule B1)] The side condition of rule B1, which requires that at least one of the two slices is PENW (pe+1 ≥ pb), is insufficient to guarantee semantic preservation. For example, let s1 = ÍX[5:3] (empty) and s2 = ÍX[4:7], with X[i]=1 for all i. The condition pe1+1 = 3+1 = 4 = pb2 is satisfied, and s2 is PENW because 7+1 ≥ 4. The rule then rewrites ÍX[5:3] + ÍX[4:7] into ÍX[5:7]. The original sum is 4 (the value of s2), while the rewritten sum is 3 (indices 5,6,7), so the rewrite is not equivalence-preserving. The correct condition must ensure that any empty slice is adjacent to the other slice in the sense that its lower bound equals pe+1 when it is empty; the current 'at least one PENW' condition does not enforce this.
  3. [§5 (overall solver soundness; §5.3 and Algorithm 2)] The paper asserts that the simplification rules and the Fourier-Motzkin adaptation are sound, but it provides no formal statement or proof of semantic preservation, and the two concrete errors above show that the informal claim is not reliable. Furthermore, several load-bearing pieces are explicitly omitted: the implementation of the IFP verification after Fig. 7 is stated to be 'not shown', the two additional B-rules in §5.3 are not shown, and BijF2 refers to 'other cases' without presenting them. For a verification paper whose central claim is that a successful solver answer implies the property actually holds, the full set of simplification rules, or a precise soundness argument covering the complete algorithm, is essential. The current level of detail is insufficient for the reader to establish trust in the system's correctness.
minor comments (6)
  1. [§2.2, Fig. 14; §5.3] The semantics of the slice sum notation ÍX[pb:pe] is never defined. The rules 0Sum, UnAft1, and UnAft3 imply that the interval is inclusive of both bounds, but this should be stated explicitly at first use to avoid off-by-one misunderstandings.
  2. [§5.3, Fig. 15 (UnBef)] Under the inclusive interval convention, the UnBef rule is sound, but the premise should also require that the index pb-1 is a legal array index (i.e., pb ≥ 1). This is likely an invariant of the equivalence table, but it should be stated as a side condition.
  3. [§5.3, Fig. 15 (B5)] In rule B5, the notation 'Z = DPR z' appears to be a typo for 'Z = DOR z', matching the DOR convention used elsewhere.
  4. [Fig. 14, legend] The line 'Rcd, Img = denotes an integral interval' is a fragment; it should be completed, e.g., as 'Rcd and Img denote integral intervals'.
  5. [§1, first paragraph] The word 'fissed' in 'the computation is separated (fissed) into bulk-parallel array operations' is unusual; if 'fused' was intended, please correct it.
  6. [§6, Fig. 17] The abstract and text mention an 'average verification time of 1 second', but Figure 17 lists individual check times (0.7, 0.1, 0.4, 0.6, 3.6, 0.3, 1.6 seconds) without an average. Adding an average row or explicitly stating that these values average to roughly 1 second would make the claim easier to verify.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the derivation chain is self-contained and benchmarks are empirical, not fitted.

full rationale

The paper's derivation chain is self-contained: InfIxf converts source programs into index functions (Figs. 9 and 12), PM reduces property verification to queries (Figs. 6-8), and QS discharges those queries by Fourier-Motzkin elimination plus simplification rules (Algorithms 1-2 and Fig. 15). No property is assumed as a premise in its own proof; properties recorded in Delta come from user preconditions or from previously verified properties, and high-level rules such as DeltaUeBij compose already-proven facts. The claimed speedups come from empirically removing dynamic checks on GPU benchmarks, not from quantities fitted to those benchmarks, so there is no fitted-input-called-prediction pattern. The paper does rely on prior work by the same authors for the Futhark compiler and for some background analyses, but those citations provide implementation and infrastructure context, not the load-bearing proof steps. The main identifiable risk is a soundness question about the simplification engine in Section 5.3, including an apparent edge case in the UnBef precondition; that is a correctness concern, not circular reasoning. Overall, no circular step can be exhibited, so the appropriate score is 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters are fitted; the framework verifies user-supplied or inferred properties. The main assumptions are standard mathematical facts and domain-specific semantic assumptions about Futhark's combinators.

assumptions (3)
  • standard math Integer arithmetic and Fourier-Motzkin elimination are sound for the polynomial inequalities generated by the query solver.
    Assumed background; the solver relies on the triangular Ranges and Equivs tables to terminate (Section 5.2).
  • domain assumption Scatter in Futhark is pure and idempotent; duplicate indices must have equal values.
    Section 2.1 states the semantics and that it is ensured by uniqueness types, but the verifier must check safety.
  • domain assumption Index functions with guarded expressions accurately capture the semantics of all supported programs, including segmented and empty segments.
    Sections 2.2 and 4 present the representation and rewriting rules without a formal soundness proof that every program maps to a faithful index function.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language." pith.science (2026). https://pith.science/paper/7RZUTTNJ

@misc{pith2026250623058,
  author       = {Pith},
  title        = {Pith review of: Verifying Properties of Index Arrays in a Purely-Functional Data-Parallel Language},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7RZUTTNJ}},
  note         = {Machine review of arXiv:2506.23058}
}
read the original abstract

This paper presents a novel approach to automatically verify properties of pure data-parallel programs with non-linear indexing -- expressed as pre- and post-conditions on functions. Programs consist of nests of second-order array combinators (e.g., map, scan, and scatter) and loops. The key idea is to represent arrays as index functions: programs are index function transformations over which properties are propagated and inferred. Our framework proves properties on index functions by distilling them into algebraic (in)equalities and discharging them to a Fourier-Motzkin-based solver. The framework is practical and accessible: properties are not restricted to a decidable logic, but instead are carefully selected to express practically useful guarantees that can be automatically reasoned about and inferred. These guarantees extend beyond program correctness and can be exploited by the entire compiler pipeline for optimization. We implement our system in the pure data-parallel language Futhark and demonstrate its practicality on seven applications, reporting an average verification time of 1 second. Two case studies show how eliminating dynamic verification in GPU programs results in significant speedups.

Figures

Figures reproduced from arXiv: 2506.23058 by the authors.

Figure 1
Figure 1. Grammar for source language expressions ( [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Running Examples: two-way partitioning (left) with demo (center) & building flag and II arrays (right). [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Grammar for symbols (𝑐), polynomials (𝑒), guarded expressions (𝑔), and index functions (𝑖𝑥 𝑓 𝑛). 𝑥𝑠 of matching length. It returns a flat array of length equal to the sum of the shapes (see the postcondition), such that each non-empty segment starts with the corresponding element of 𝑥𝑠 and the rest of the segment is zeroed. For example, if 𝑠ℎ𝑎𝑝𝑒 = [0, 2, 1, 0, 3] and 𝑥𝑠 = [1, 2, 3, 4, 5] then 𝑚𝑘𝑆𝑔𝑚𝐷𝑒𝑠𝑐𝑟 𝑠ℎ𝑎𝑝𝑒 𝑥𝑠 = [… view at source ↗
Figures from the paper (13 more)
Figure 4
Figure 4. Figure 4: Bird’s Eye View of the Three Logical Components of the Framework, which are deeply connected. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Array Properties. 𝑋, 𝑌, 𝜎 are array variables; 𝑝 denotes a predicate in lambda form of type 𝑖𝑛𝑡 → 𝑏𝑜𝑜𝑙. trivial, cannot produce useful index functions for their results. Finally, the query solver (QS) uses the properties in Δ to solve (in)equalities by extending Fourie…
Figure 6
Figure 6. Figure 6: Verifying injectivity and bijectivity of variables and index functions denoting arrays. [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: Guarded Expressions Helpers & Translating Filter-Partitioning Property to Inverse Filtering Partitioning [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]
Figure 8
Figure 8. Figure 8: Inferring and Verifying Properties at a High Level. [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]
Figure 9
Figure 9. Figure 9: Converting the source language to index functions. [PITH_FULL_IMAGE:figures/full_fig_p013_9.png]
Figure 11
Figure 11. Figure 11: Rewrite rules for index functions. 𝑒2) Ó (𝑐3 ⇒ 𝑒3). Similarly, K ⟨𝑒⟩ denotes the symbol (or expression) obtained by replacing □ with 𝑒 in the context K. For example, if K = 𝑒1 + 𝑥1 [□], then K ⟨𝑥2⟩ is K = 𝑒1 + 𝑥1 [𝑥2]. Reductions are used in the rewrite rules shown in…
Figure 12
Figure 12. Figure 12: Additional rewrite rules as well as conversion of [PITH_FULL_IMAGE:figures/full_fig_p015_12.png]
Figure 13
Figure 13. Figure 13: Substitution rules for segmented domains. [PITH_FULL_IMAGE:figures/full_fig_p016_13.png]
Figure 14
Figure 14. Figure 14: Grammar for symbols (𝑠), polynomial (𝑃𝑜𝑙𝑦) and guarded expressions (𝑔), and index functions 𝑖𝑥 𝑓 𝑛. substitutions. The source program is converted top-to-bottom; top-level functions must be declared before using them. This means all top-level functions have index func…
Figure 15
Figure 15. Figure 15: Rules for Unary and Binary Simplification of Expressions in Polynomial Representation. [PITH_FULL_IMAGE:figures/full_fig_p019_15.png]
Figure 16
Figure 16. Figure 16: Compute kernels from Maximal Matching (left) and sparse [PITH_FULL_IMAGE:figures/full_fig_p021_16.png]
Figure 17
Figure 17. Figure 17: Left: Summary of evaluated programs. IFP and FP abbreviate InvFiltPart and FiltPart, respectively. [PITH_FULL_IMAGE:figures/full_fig_p022_17.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

73 extracted references · 52 canonical work pages

  1. [1]

    Blelloch, Laxman Dhulipala, Magdalen Dobson, and Yihan Sun

    Daniel Anderson, Guy E. Blelloch, Laxman Dhulipala, Magdalen Dobson, and Yihan Sun. 2022. The problem-based benchmark suite (PBBS), V2. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Seoul, Republic of Korea) (PPoPP ’22). Association for Computing Machinery, New York, NY, USA, 445–447. https://doi.org/...

    arXiv 2022

  2. [2]

    Lubin Bailly, Troels Henriksen, and Martin Elsman. 2023. Shape-Constrained Array Programming with Size-Dependent Types. In Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing. 29–41

    work page 2023

  3. [3]

    Ziogas, Timo Schneider, and Torsten Hoefler

    Tal Ben-Nun, Johannes de Fine Licht, Alexandros N. Ziogas, Timo Schneider, and Torsten Hoefler. 2019. Stateful Dataflow Multigraphs: A Data-Centric Model for Performance Portability on Heterogeneous Architectures. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC ’19) . ACM, Article 81, 14 ...

    arXiv 2019

  4. [4]

    Elbert, Rhea George, Jeremy McGibbon, Lukas Trümper, Elynn Wu, Oliver Fuhrer, Thomas Schulthess, and Torsten Hoefler

    Tal Ben-Nun, Linus Groner, Florian Deconinck, Tobias Wicky, Eddie Davis, Johann Dahm, Oliver D. Elbert, Rhea George, Jeremy McGibbon, Lukas Trümper, Elynn Wu, Oliver Fuhrer, Thomas Schulthess, and Torsten Hoefler. 2022. Productive performance engineering for weather and climate modeling with Python. In Proceedings of the International Conference for High ...

    work page 2022

  5. [5]

    Yves Bertot and Pierre Castéran. 2013. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media. 8One example is the Brownian Bridge component of the option pricing describe in [40], which uses three indirect arrays. , Vol. 1, No. 1, Article . Publication date: September 2025....

    work page 2013

  6. [6]

    Blelloch

    Guy E. Blelloch. 1989. Scans as Primitive Parallel Operations. Computers, IEEE Transactions 38, 11 (1989), 1526–1538

    work page 1989

  7. [7]

    Blelloch and John Greiner

    Guy E. Blelloch and John Greiner. 1996. A Provable Time and Space Efficient Implementation of NESL. In Proceedings of the First ACM SIGPLAN International Conference on Functional Programming (Philadelphia, Pennsylvania, USA) (ICFP ’96). ACM, New York, NY, USA, 213–225. https://doi.org/10.1145/232627.232650

    work page arXiv 1996

  8. [8]

    Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. 2005. Permission accounting in separation logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Long Beach, California, USA) (POPL ’05). Association for Computing Machinery, New York, NY, USA, 259–270. https: //doi.org/10.1145/1040305.1040327

    arXiv 2005

Show all 73 references
  1. [9]

    Ana Bove, Peter Dybjer, and Ulf Norell. 2009. A brief overview of Agda–a functional language with dependent types. In Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20,

    2009

  2. [10]

    Aaron R Bradley, Zohar Manna, and Henny B Sipma. 2006. What’s decidable about arrays?. In Verification, Model Checking, and Abstract Interpretation: 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10,

    2006

  3. [11]

    Stephen Brookes and Peter W O’Hearn. 2016. Concurrent separation logic. ACM SIGLOG News 3, 3 (2016), 47–65

    2016

  4. [12]

    Chakravarty, Gabriele Keller, Sean Lee, Trevor L

    Manuel M.T. Chakravarty, Gabriele Keller, Sean Lee, Trevor L. McDonell, and Vinod Grover. 2011. Accelerating Haskell array codes with multicore GPUs. In Proceedings of the Sixth Workshop on Declarative Aspects of Multicore Programming (Austin, Texas, USA) (DAMP ’11). Associati...

    2011

  5. [13]

    Chicha, M

    Y. Chicha, M. Lloyd, C. Oancea, and S. M. Watt. 2004. Parametric Polymorphism for Computer Algebra Software Components. In Procs. of the 6th Int. Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC ’04). Mirton Publishing House, 119–130

    2004

  6. [14]

    Basile Clément and Albert Cohen. 2022. End-to-end translation validation for the halide language. 6, OOPSLA1, Article 84 (April 2022), 30 pages. https://doi.org/10.1145/3527328

    2022 doi

  7. [15]

    Przemysław Daca, Thomas A Henzinger, and Andrey Kupriyanov. 2016. Array folds logic. In International Conference on Computer Aided Verification. Springer, 230–248

    2016

  8. [16]

    Dang, Hao Yu, and Lawrence Rauchwerger

    Francis H. Dang, Hao Yu, and Lawrence Rauchwerger. 2002. The R-LRPD Test: Speculative Parallelization of Partially Parallel Loops. In Proceedings of the 16th International Parallel and Distributed Processing Symposium (IPDPS ’02) . IEEE Computer Society, USA

    2002

  9. [17]

    Leonardo de Moura and Nikolaj Bjørner. 2007. Efficient E-Matching for SMT Solvers. In Automated Deduction – CADE-21, Frank Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 183–198

    2007

  10. [18]

    Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: an efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) (TACAS’08/ETAPS’08). Springer...

    2008

  11. [19]

    van Balen, Gabriele K

    Ivo Gabe de Wolff, David P. van Balen, Gabriele K. Keller, and Trevor L. McDonell. 2024. Zero-Overhead Parallel Scans for Multi-Core CPUs. In Proceedings of the 15th International Workshop on Programming Models and Applications for Multicores and Manycores (PMAM ’24) . Associa...

    2024 doi

  12. [20]

    Chen Ding and Ken Kennedy. 1999. Improving cache performance in dynamic applications through data and computa- tion reorganization at run time. In Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation (Atlanta, Georgia, USA) (PLDI ’99...

    1999

  13. [21]

    Joseph Fourier. 1827. Histoire de l’Académie, partie mathématique (1824). Mémoires de l’Académie des sciences de l’Institut de France 7 (1827)

  14. [22]

    Bastian Hagedorn, Larisa Stoltzfus, Michel Steuwer, Sergei Gorlatch, and Christophe Dubach. 2018. High Performance Stencil Code Generation with Lift. In Int. Symposium on Code Generation and Optimization (CGO) (Vienna, Austria) (CGO 2018). ACM, 100–112. https://doi.org/10.1145/3168824

    2018 doi

  15. [23]

    Oancea, Anne Elster, Ari Rasch, Sameeran Joshi, Amir Mohammad Tavakkoli, and Richard Schulze

    Mary Hall, Cosmin E. Oancea, Anne Elster, Ari Rasch, Sameeran Joshi, Amir Mohammad Tavakkoli, and Richard Schulze. 2025. Scheduling Language Chronology: Past, Present, and Future. ACM Trans. Archit. Code Optim. (June 2025). https://doi.org/10.1145/3743135

    2025 doi

  16. [24]

    Hall, Saman P

    Mary W. Hall, Saman P. Amarasinghe, Brian R. Murphy, Shih-Wei Liao, and Monica S. Lam. 2005. Interprocedural Parallelization Analysis in SUIF. Trans. on Prog. Lang. and Sys. (TOPLAS) 27(4) (2005), 662–731

    2005

  17. [25]

    Maxwell Harper and Joseph A

    F. Maxwell Harper and Joseph A. Konstan. 2015. The MovieLens Datasets: History and Context. ACM Trans. Interact. Intell. Syst. 5, 4, Article 19 (Dec. 2015), 19 pages. https://doi.org/10.1145/2827872

    2015 doi

  18. [26]

    Troels Henriksen. 2017. Design and Implementation of the Futhark Programming Language . Ph. D. Dissertation. University of Copenhagen, Universitetsparken 5, 2100 Copenhagen

    2017

  19. [27]

    Troels Henriksen. 2021. Bounds checking on GPU. International Journal of Parallel Programming 49, 6 (2021), 761–775. , Vol. 1, No. 1, Article . Publication date: September 2025. 26 Nikolaj Hey Hinnerskov, Robert Schenck, and Cosmin E. Oancea

    2021

  20. [28]

    Troels Henriksen and Martin Elsman. 2021. Towards Size-Dependent Types for Array Programming. In Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming (Virtual, Canada) (ARRAY 2021). Association for Computing Mach...

    2021

  21. [29]

    Troels Henriksen, Sune Hellfritzsch, Ponnuswamy Sadayappan, and Cosmin Oancea. 2020. Compiling Generalized Histograms for GPU. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (Atlanta, Georgia) (SC ’20). IEEE Pres...

    2020

  22. [30]

    Troels Henriksen and Cosmin E. Oancea. 2014. Bounds Checking: An Instance of Hybrid Analysis. In Proceedings of ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming (ARRAY’14) . Association for Computing Machinery, New York, NY, USA, ...

    2014

  23. [31]

    Troels Henriksen, Niels GW Serup, Martin Elsman, Fritz Henglein, and Cosmin E Oancea. 2017. Futhark: purely functional GPU-programming with nested parallelism and in-place array updates. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Imple...

    2017

  24. [32]

    Troels Henriksen, Frederik Thorøe, Martin Elsman, and Cosmin Oancea. 2019. Incremental Flattening for Nested Data Parallelism. In Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming (Washington, District of Columbia) (PPoPP ’19). ACM, New York,...

    2019

  25. [33]

    Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr

    Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021). ...

    2021

  26. [34]

    Lopes, David Menendez, Santosh Nagarakatte, and John Regehr

    Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2018. Practical verification of peephole optimizations with Alive. Commun. ACM 61, 2 (Jan. 2018), 84–91. https://doi.org/10.1145/3166064

    2018 doi

  27. [35]

    Sungdo Moon and Mary W. Hall. 1999. Evaluation of predicated array data-flow analysis for automatic parallelization. In Proceedings of the Seventh ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Atlanta, Georgia, USA) (PPoPP ’99). Association for Comp...

    1999

  28. [36]

    Philip Munksgaard, Svend Lund Breddam, Troels Henriksen, Fabian Cristian Gieseke, and Cosmin Oancea. 2021. Dataset Sensitive Autotuning of Multi-versioned Code Based on Monotonic Properties. In Trends in Functional Programming, Viktória Zsók and John Hughes (Eds.). Springer In...

    2021

  29. [38]

    Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodik, and Shoaib Kamil

    Julie L. Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodik, and Shoaib Kamil. 2020. Verifying and improving Halide’s term rewriting system with program synthesis. Proc. ACM Program. Lang. 4, OOPSLA, Article 166 (Nov. 2020), 28 pages. https://doi.org/10.1145/3428234

    2020 doi

  30. [39]

    Corey J Nolet, Divye Gala, Edward Raff, Joe Eaton, Brad Rees, John Zedlewski, and Tim Oates. 2022. GPU semiring primitives for sparse neighborhood methods. Proceedings of Machine Learning and Systems 4 (2022), 95–109

    2022

  31. [40]

    Oancea, Christian Andreetta, Jost Berthold, Alain Frisch, and Fritz Henglein

    Cosmin E. Oancea, Christian Andreetta, Jost Berthold, Alain Frisch, and Fritz Henglein. 2012. Financial software on GPUs: between Haskell and Fortran. In Proceedings of the 1st ACM SIGPLAN Workshop on Functional High-Performance Computing (FHPC ’12) . Association for Computing...

    2012

  32. [41]

    Oancea and Alan Mycroft

    Cosmin E. Oancea and Alan Mycroft. 2008. Set-Congruence Dynamic Analysis for Thread-Level Speculation (TLS) . Springer-Verlag, Berlin, Heidelberg, 156–171. https://doi.org/10.1007/978-3-540-89740-8_11

    2008 doi

  33. [42]

    Oancea and Lawrence Rauchwerger

    Cosmin E. Oancea and Lawrence Rauchwerger. 2013. A Hybrid Approach to Proving Memory Reference Monotonicity. In Languages and Compilers for Parallel Computing , Sanjay Rajopadhye and Michelle Mills Strout (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 61–75

    2013

  34. [43]

    Oancea and Lawrence Rauchwerger

    Cosmin E. Oancea and Lawrence Rauchwerger. 2015. Scalable Conditional Induction Variables (CIV) Analysis. In Proceedings of the 13th Annual IEEE/ACM International Symposium on Code Generation and Optimization (San Francisco, California) (CGO ’15). IEEE Computer Society, Washin...

    2015

  35. [44]

    Cosmin Eugen Oancea, Ties Robroek, and Fabian Gieseke. 2020. Approximate Nearest-Neighbour Fields via Massively- Parallel Propagation-Assisted K-D Trees. In 2020 IEEE International Conference on Big Data (Big Data) . 5172–5181. https://doi.org/10.1109/BigData50022.2020.9378426

    2020

  36. [45]

    Oancea, Jason W

    Cosmin E. Oancea, Jason W. A. Selby, Mark Giesbrecht, and Stephen M. Watt. 2005. Distributed Models of Thread-Level Speculation. In Procs. of the Int. Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA ’05). 920–927

    2005

  37. [46]

    Oancea and Stephen M

    Cosmin E. Oancea and Stephen M. Watt. 2005. Parametric polymorphism for software component architectures. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA ’05). Association for Computing Machi...

    2005

  38. [47]

    Yunheung Paek, Jay Hoeflinger, and David Padua. 2002. Efficient and Precise Array Access Analysis. Trans. on Prog. Lang. and Sys. (TOPLAS) 24(1) (2002), 65–109

    2002

  39. [48]

    Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand, and Saman Amarasinghe

  40. [49]

    Rondon, Ming Kawaguci, and Ranjit Jhala

    Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. [n. d.]. Liquid types. InProceedings of the 29th ACM SIGPLAN Con- ference on Programming Language Design and Implementation (New York, NY, USA, 2008-06-07) (PLDI ’08). Association for Computing Machinery, 159–169. https://doi...

    2008

  41. [50]

    Silvius Rus, Lawrence Rauchwerger, and Jay Hoeflinger. 2002. Hybrid analysis: static & dynamic memory reference analysis. In Proceedings of the 16th International Conference on Supercomputing (ICS ’02) . Association for Computing Machinery, 274–284. https://doi.org/10.1145/514...

    2002

  42. [51]

    Amr Sabry and Matthias Felleisen. 1992. Reasoning About Programs in Continuation-passing Style. SIGPLAN Lisp Pointers V, 1 (Jan. 1992), 288–298

    1992

  43. [52]

    Robert Schenck, Ola Rønning, Troels Henriksen, and Cosmin E. Oancea. 2022. AD for an array language with nested parallelism. In Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (Dallas, Texas) (SC ’22). IEEE Press, Art...

    2022 arXiv

  44. [53]

    Dmitry Serykh, Stefan Oehmcke, Cosmin Oancea, Dainius Masili¯unas, Jan Verbesselt, Yan Cheng, Stéphanie Horion, Fabian Gieseke, and Nikolaj Hinnerskov. 2023. Seasonal-Trend Time Series Decomposition on Graphics Processing Units. In IEEE International Conference on Big Data (Bi...

    2023

  45. [54]

    Wilfried Sieg and Barbara Kauffmann. 1993. Unification for quantified formulae . Carnegie Mellon [Department of Philosophy]

    1993

  46. [55]

    Michel Steuwer, Christian Fensch, Sam Lindley, and Christophe Dubach. 2015. Generating performance portable code using rewrite rules: from high-level functional expressions to high-performance OpenCL code. In Proceedings of the 20th ACM SIGPLAN International Conference on Func...

    2015

  47. [56]

    Steuwer, T

    M. Steuwer, T. Koehler, B. Köpcke, and F. Pizzuti. 2022. RISE & Shine: Language-Oriented Compiler Design. arXiv:2201.03611 [cs.PL]

    2022 arXiv

  48. [57]

    Michelle Mills Strout and Paul D. Hovland. 2004. Metrics and models for reordering transformations. In Proceedings of the 2004 Workshop on Memory System Performance (Washington, D.C.)(MSP ’04). Association for Computing Machinery, New York, NY, USA, 23–34. https://doi.org/10.1...

    2004

  49. [58]

    Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. 2016. Dependent types and multi-monadic effects in F. InProceedings of the 43rd annual ACM SI...

    2016

  50. [59]

    Nikhil Swamy, Guido Martínez, and Aseem Rastogi. 2023. Proof-Oriented Programming in F

    2023

  51. [60]

    Kai Trojahner and Clemens Grelck. 2009. Dependently typed array programs don’t go wrong. The Journal of Logic and Algebraic Programming 78, 7 (2009), 643–664. https://doi.org/10.1016/j.jlap.2009.03.002 The 19th Nordic Workshop on Programming Theory (NWPT 2007)

    2009 doi

  52. [61]

    van den Haak, Trevor L

    Lars B. van den Haak, Trevor L. McDonell, Gabriele K. Keller, and Ivo Gabe de Wolff. 2020. Accelerating Nested Data Parallelism: Preserving Regularity. In Euro-Par 2020: Parallel Processing , Maciej Malawski and Krzysztof Rzadca (Eds.). Springer International Publishing, Cham, 426–442

    2020

  53. [62]

    van den Haak, Anton Wijs, Marieke Huisman, and Mark van den Brand

    Lars B. van den Haak, Anton Wijs, Marieke Huisman, and Mark van den Brand. 2024. HaliVer: Deductive Verification and Scheduling Languages Join Forces. In Tools and Algorithms for the Construction and Analysis of Systems , Bernd Finkbeiner and Laura Kovács (Eds.). Springer Natu...

    2024

  54. [63]

    Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones

    Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. SIGPLAN Not. 49, 9 (Aug. 2014), 269–282. https://doi.org/10.1145/2692915.2628161

    2014

  55. [64]

    Scott, Ryan R

    Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. [n. d.]. Refinement reflection: complete verification with SMT. 2 ([n. d.]), 1–31. Issue POPL. https://doi.org/10.1145/ 3158141

  56. [65]

    Sven Verdoolaege, Juan Carlos Juega, Albert Cohen, José Ignacio Gómez, Christian Tenllado, and Francky Catthoor

  57. [66]

    H Paul Williams. 1986. Fourier’s Method of Linear Programming and its Dual.The American Mathematical Monthly 93, 9 (1986), 681–695. https://doi.org/10.1080/00029890.1986.11971923 arXiv:https://doi.org/10.1080/00029890.1986.11971923

    1986

  58. [67]

    Hongwei Xi. 2007. Dependent ML An approach to practical programming with dependent types. Journal of Functional Programming 17, 2 (2007), 215–286. https://doi.org/10.1017/S0956796806006216 , Vol. 1, No. 1, Article . Publication date: September 2025. 28 Nikolaj Hey Hinnerskov, ...

    2007 doi

  59. [68]

    Hongwei Xi. 2017. Applied type system: An approach to practical programming with theorem-proving. arXiv preprint arXiv:1703.08683 (2017)

    2017 arXiv

  60. [69]

    ACM Trans

    Polyhedral Parallel Code Generation for CUDA. ACM Trans. Archit. Code Optim. 9, 4, Article 54 (Jan. 2013), 23 pages. https://doi.org/10.1145/2400682.2400713

    2013

  61. [70]

    Alexandros Nikolaos Ziogas, Tal Ben-Nun, Guillermo Indalecio Fernández, Timo Schneider, Mathieu Luisier, and Torsten Hoefler. 2019. A data-centric approach to extreme-scale ab initio dissipative quantum transport simulations. In Proceedings of the International Conference for ...

    2019

  62. [73]

    Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (Montreal, Quebec, Canada) (PLDI ’98). Association for Computing Machinery, New Yo...

    1998

  63. [2006]

    Springer, 427–442

    Proceedings 7. Springer, 427–442

  64. [2009]

    Springer, 73–78

    Proceedings 22. Springer, 73–78

  65. [2013]

    In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI ’13)

    Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI ’13). ACM, New York, NY, ...

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.