We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
FORMAL PROOFS OF FUNCTIONAL BSP PROGRAMS.
- Authors
Gava, Frédéric
- Abstract
The Bulk Synchronous Parallel ML (BSML) is a functional language for BSP programming, a model of computing which allows parallel programs to be ported to a wide range of architectures. It is based on an extension of the ML language by parallel operations on a parallel data structure called parallel vector, which is given by intention. We present a new approach to certifying BSML programs in the context of type theory. Given a specification and a program, an incomplete proof of the specification (of which algorithmic contents corresponds to the given program) is built in the type theory, in which gaps would correspond to the proof obligation. This development demonstrates the usefulness of higher-order logic in the process of software certification of parallel applications. It also shows that the proof of rather complex parallel algorithms may be done with inductive types without great difficulty by using existing certified programs. This work has been implemented in the Coq Proof Assistant, applied on non-trivial examples and is the basis of a certified library of BSML programs.
- Subjects
PARALLEL programming; PROGRAMMING languages; TYPE theory
- Publication
Parallel Processing Letters, 2003, Vol 13, Issue 3, p365
- ISSN
0129-6264
- Publication type
Article
- DOI
10.1142/S0129626403001343