Refinement of parallel algorithms down to LLVM

DOI10.4230/LIPICS.ITP.2022.24MaRDI QIDQ6572562zbMATH OpenFDO

Authors Peter Lammich

Publication date 15 July 2024

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2022.24

zbMATH Keywords

concurrent separation logicparallel sortingLLVMisabelle

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(3)

• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• A generalised union of rely-guarantee and separation logic using permission algebras
• Preserving provability over GPU program optimizations with annotation-aware transformations

This page was built for publication: Refinement of parallel algorithms down to LLVM

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6572562)