A constructive denotational semantics for Kahn networks in Coq

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.
Type de document :
Chapitre d'ouvrage
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

Littérature citée [14 références]

https://hal.inria.fr/inria-00431806
Contributeur : Christine Paulin-Mohring <>
Soumis le : vendredi 13 novembre 2009 - 10:56:53
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : mardi 16 octobre 2012 - 13:56:02

Fichier

postprint.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

• HAL Id : inria-00431806, version 1

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〉

Métriques

Consultations de la notice

367

Téléchargements de fichiers