TowardsVerified Scalable Parallel Computing with Coqand Spark

被引：2
|
作者：
Loulergue, Frederic [1 ]
Philippe, Jolan [2 ]
机构：
[1] Univ Orleans, INSA CVL, LIFO, EA 4022, Orleans, France
[2] IMT Atlantique, INRIA, LS2N, CNRS,UMR 6004, Nantes, France
来源：
PROCEEDINGS OF THE 25TH ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS, FTFJP 2023 | 2023年
关键词：
Interactive theorem proving; Program transformation; Coq; Scala; Apache Spark; Algorithmic skeletons; Functional programming; FORMAL VERIFICATION; PROGRAMS; MODEL;
D O I：
10.1145/3605156.3606450
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.
引用
收藏
页码：11 / 17
页数：7
相关论文
共 50 条
  • [21] HRV-Spark: Computing Heart Rate Variability Measures Using Apache Spark
    Qu, Xufeng
    Wu, Yuanyuan
    Liu, Jinze
    Cui, Licong
    2020 IEEE INTERNATIONAL CONFERENCE ON BIOINFORMATICS AND BIOMEDICINE, 2020, : 2235 - 2241
  • [22] An Overview of Hadoop MapReduce, Spark, and Scalable Graph Processing Architecture
    Talan, Pooja P.
    Sharma, Kartik U.
    Nawade, Pratiksha P.
    Talan, Karishma P.
    RECENT DEVELOPMENTS IN MACHINE LEARNING AND DATA ANALYTICS, 2019, 740 : 35 - 42
  • [23] A fast scalable distributed kriging algorithm using Spark framework
    Misra, Chandan
    Bhattacharya, Sourangshu
    Ghosh, Soumya K.
    INTERNATIONAL JOURNAL OF DATA SCIENCE AND ANALYTICS, 2020, 10 (03) : 249 - 264
  • [24] SPIN: A Fast and Scalable Matrix Inversion Method in Apache Spark
    Misra, Chandan
    Haldar, Swastik
    Bhattacharya, Sourangshu
    Ghosh, Soumya K.
    ICDCN'18: PROCEEDINGS OF THE 19TH INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING AND NETWORKING, 2018,
  • [25] A fast scalable distributed kriging algorithm using Spark framework
    Chandan Misra
    Sourangshu Bhattacharya
    Soumya K. Ghosh
    International Journal of Data Science and Analytics, 2020, 10 : 249 - 264
  • [26] From distributed sequential computing to distributed parallel computing
    Pan, L
    Bic, LF
    Dillencourt, MB
    Lai, MK
    2003 INTERNATIONAL CONFERENCE ON PARALLEL PROCESSING WORKSHOPS, PROCEEDINGS, 2003, : 255 - 262
  • [27] A Speculative Parallel Execution Model for Apache Spark
    Wang, Zhoukai
    Zhao, Yinliang
    PROCEEDINGS OF 2018 IEEE 9TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), 2018, : 84 - 89
  • [28] Scalable Online-Offline Stream Clustering in Apache Spark
    Backhoff, Omar
    Ntoutsi, Eirini
    2016 IEEE 16TH INTERNATIONAL CONFERENCE ON DATA MINING WORKSHOPS (ICDMW), 2016, : 37 - 44
  • [29] Parallel Computing: Review and Perspective
    Li, Yuxiang
    Zhang, Zhiyong
    2018 5TH INTERNATIONAL CONFERENCE ON INFORMATION SCIENCE AND CONTROL ENGINEERING (ICISCE 2018), 2018, : 365 - 369
  • [30] Parallel Computing for Brain Simulation
    Pastur-Romay, L. A.
    Porto-Pazos, A. B.
    Cedron, F.
    Pazos, A.
    CURRENT TOPICS IN MEDICINAL CHEMISTRY, 2017, 17 (14) : 1646 - 1668
12345