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 条

[41] A Fast Parallel Random Forest Algorithm Based on Spark
Yin, Linzi
Chen, Ken
Jiang, Zhaohui
Xu, Xuemei
APPLIED SCIENCES-BASEL, 2023, 13 (10):
[42] Design and Development of Scalable SIEM as a Service using Spark and Anomaly Detection
Thepa, Thean
Ateetanan, Pongsapon
Khubpatiwitthayakul, Pratuck
Fugkeaw, Somchart
2024 21ST INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING, JCSSE 2024, 2024, : 199 - 205
[43] Non-reversible parallel tempering: A scalable highly parallel MCMC scheme
Syed, Saifuddin
Bouchard-Cote, Alexandre
Deligiannidis, George
Doucet, Arnaud
JOURNAL OF THE ROYAL STATISTICAL SOCIETY SERIES B-STATISTICAL METHODOLOGY, 2022, 84 (02) : 321 - 350
[44] Spark-IDPP: high-throughput and scalable prediction of intrinsically disordered protein regions with Spark clusters on the Cloud
Malysiak-Mrozek, Bozena
Baron, Tomasz
Mrozek, Dariusz
CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 2019, 22 (02): : 487 - 508
[45] Spark-IDPP: high-throughput and scalable prediction of intrinsically disordered protein regions with Spark clusters on the Cloud
Bożena Małysiak-Mrozek
Tomasz Baron
Dariusz Mrozek
Cluster Computing, 2019, 22 : 487 - 508
[46] Parallel computing efficiency of SWAN 40.91
Rautenbach, Christo
Mullarney, Julia C.
Bryan, Karin R.
GEOSCIENTIFIC MODEL DEVELOPMENT, 2021, 14 (07) : 4241 - 4247
[47] RETRACTED: Application of Spark big data system and network convolution parallel computing in the analysis of Mirsky's works in comparative literature (Retracted Article)
Dai, Keke
JOURNAL OF AMBIENT INTELLIGENCE AND HUMANIZED COMPUTING, 2021, 13 (Suppl 1) : 17 - 17
[48] A Comprehensive Exploration of Languages for Parallel Computing
Ciccozzi, Federico
Addazi, Lorenzo
Asadollah, Sara Abbaspour
Lisper, Bjorn
Masud, Abu Naser
Mubeen, Saad
ACM COMPUTING SURVEYS, 2023, 55 (02)
[49] Performance Evaluation of Residential Demand Response Based on a Modified Fuzzy VIKOR and Scalable Computing Method
Dong, Jun
Li, Rong
Huang, Hui
ENERGIES, 2018, 11 (05)
[50] Spark framework based on a heterogenous pipeline computing with open CL
Kim D.
Park N.
Transactions of the Korean Institute of Electrical Engineers, 2018, 67 (02) : 270 - 276

← 1 2 3 4 5 →