| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 488133 | Procedia Computer Science | 2011 | 10 Pages |
Abstract
Bulk Synchronous Parallel ML (BSML) is a structured parallel functional programming language. It extends a functional programming language of the ML family with a polymorphic data structure and a very small set of primitives. In this paper we describe a framework for reasoning about BSML programs using the Coq interactive theorem prover and for extracting actual parallel programs from proofs. This framework is illustrated through a simulation application based on heat equation.
Related Topics
Physical Sciences and Engineering
Computer Science
Computer Science (General)
