A constructive denotational semantics for Kahn networks in Coq

Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn's scientic contributions. In his paper \The semantics of a simple language for parallel programming" (11), he proposed an interpre- tation of (deterministic) parallel programs (now called Kahn networks) as stream transformers based on the theory of complete partial orders (cpos). A restriction of this language to synchronous programs is the basis of the data-ow Lustre language which is used for the development of critical embedded systems (14, 10). We present a formalization of this seminal paper in the Coq proof assistant (4, 15). For that purpose, we developed a general library for cpos. Our cpos are dened with an explicit function computing the least upper bound (lub) of an increasing sequence of elements. This is dierent from what Kahn developed for the standard Coq library where only the existence of lubs (for arbitrary directed sets) is required, giving no way to explicitly compute a xpoint. We dene a cpo structure for the type of possibly innite streams. It is then possible to dene formally what is a Kahn network and what is its semantics, achieving the goal of having the concept closed under composition and recursion. The library is illustrated with an example taken from the original paper as well as the Sieve of Eratosthenes, an example of a dynamic network.