A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation

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.