SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs
摘要
The SyDPaCC framework supports the development of scalable parallel functional programs with Coq and helps the developers to write correct-by-construction programs with respect to specifications written as simple (and possibly very inefficient) functional programs. Parallel programs are built from specifications using verified program transformations offered by SyDPaCC. Leveraging the Coq extraction mechanism, compilable code can be obtained and executed on shared-memory or large scale distributed memory parallel machines. This paper presents the usage of SyDPaCC via an example, explains the internals of SyDPaCC and gives a tour of the program transformations provided by the framework.