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
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
Liste complète des métadonnées

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00431806
Contributor : Christine Paulin-Mohring <>
Submitted on : Friday, November 13, 2009 - 10:56:53 AM
Last modification on : Thursday, April 5, 2018 - 12:30:08 PM
Document(s) archivé(s) le : Tuesday, October 16, 2012 - 1:56:02 PM

File

postprint.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00431806, version 1

Collections

Citation

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〉

Share

Metrics

Record views

392

Files downloads

258