Skip to Main content Skip to Navigation
Book sections

A constructive denotational semantics for Kahn networks in Coq

Christine Paulin-Mohring 1, 2 
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Semantics of programming languages and interactive environments for the development of proofs and programs are two important aspects of Gilles Kahn's scientific contributions. In his paper ``The semantics of a simple language for parallel programming'', he proposed an interpretation 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-flow Lustre language which is used for the development of critical embedded systems. We present a formalization of this seminal paper in the Coq proof assistant. For that purpose, we developed a general library for cpos. Our cpos are defined with an explicit function computing the least upper bound (lub) of an increasing sequence of elements. This is different 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 fixpoint. We define a cpo structure for the type of possibly infinite streams. It is then possible to define 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.
Document type :
Book sections
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Christine Paulin-Mohring Connect in order to contact the contributor
Submitted on : Friday, November 13, 2009 - 10:56:53 AM
Last modification on : Sunday, June 26, 2022 - 11:50:50 AM
Long-term archiving on: : Tuesday, October 16, 2012 - 1:56:02 PM


Files produced by the author(s)


  • HAL Id : inria-00431806, version 1



Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. Yves Bertot and Gérard Huet and Jean-Jacques Lévy and Gordon Plotkin. From Semantics to Computer Science, Cambridge University Press, pp.383-413, 2009, 9780521518253. ⟨inria-00431806⟩



Record views


Files downloads