Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
Hostname: page-component-66644f4456-q629f Total loading time: 0 Render date: 2025-02-13T07:52:57.337Z Has data issue: true hasContentIssue false

17 - A constructive denotational semantics for Kahn networks in Coq

Published online by Cambridge University Press:  06 August 2010

By
Christine Paulin-Mohring
Edited by
Yves Bertot ,
Gérard Huet ,
Jean-Jacques Lévy  and
Gordon Plotkin
Christine Paulin-Mohring
Affiliation:
INRIA Saclay – Île-de-France and Université Paris-Sud
Yves Bertot
Affiliation:
INRIA-Sophia Antipolis, France
Gérard Huet
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Jean-Jacques Lévy
Affiliation:
Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt
Gordon Plotkin
Affiliation:
University of Edinburgh
Get access

Summary

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
Chapter
Information
From Semantics to Computer Science
Essays in Honour of Gilles Kahn
 , pp. 383 - 414
Publisher: Cambridge University Press
Print publication year: 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

[1]P., Audebaud and C., Paulin-Mohring. Proofs of randomized algorithms in Coq. In T., Uustalu (ed.) Mathematics of Program Construction, MPC 2006, volume 4014, Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer-Verlag, 2006.Google Scholar
[2]P., Audebaud and C., Paulin-Mohring. Proofs of randomized algorithms in Coq. To appear in Science of Computer Programming. Extended version of [1].
[3]Y., Bertot. Filters on coinductive streams, an application to Eratos thenes'sieve. In P., Urzyczyn (ed.) International Conference of Typed Lambda Calculi and Applications, volume 3461, Lecture Notes in Computer Science, pp. 102–115. Springer-Verlag, 2005.Google Scholar
[4]Y., Bertot and P., Castéran. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.Google Scholar
[5]S., Boulmé and G., Hamon. Certifying synchrony for free. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 2250, Lecture Notes in Artificial Intelligence, La Havana, Cuba, December 2001. Springer-Verlag, 2001. Short version of A clocked denotational semantics for Lucid-Synchrone in Coq, available as a Technical Report (LIP6), at www.lri.fr/∼pouzet.Google Scholar
[6]V., Capretta. General recursion via coinductive types. Logical Methods in Computer Science, 1(2:1):1–28, 2005.Google Scholar
[7]P., Caspi and M., Pouzet. Synchronous Kahn Networks. In ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pensylvania, May 1996.Google Scholar
[8]A., Cohen, M., Duranton, C., Eisenbeis, C., Pagetti, F., Plateau and M., Pouzet. N-Synchronous Kahn networks: a relaxed model of synchrony for real-time systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006.Google Scholar
[9]B., Courcelle, G., Kahn and J., Vuillemin. Algorithmes d'équivalence et de réduction à des expressions minimales dans une classe d'équations récursives simples. In J., Loeckx (ed.) Automata, Languages and Programming, volume 14, Lecture Notes in Computer Science, pp. 200–213. Springer-Verlag, 1974. Translation from French by T. Veldhuizen with original text, a few comments and additional references.Google Scholar
[10]N., Halbwachs, P., Caspi, P., Raymond and D., Pilaud. The synchronous dataflow programming language lustre. Proceedings of the IEEE, 79(9):1305–1320, 1991.Google Scholar
[11]G., Kahn. The semantics of a simple language for parallel programming. In Information Processing 74. North-Holland, 1974.Google Scholar
[12]G., Kahn and D., MacQueen. Coroutines and networks of parallel processes. In B., Gilchrist (ed.) Information Processing 77. North-Holland, 1977.Google Scholar
[13]G., Kahn and G. D., Plotkin. Concrete domains. Theoretical Computer Science, 121(1& 2):187–277, 1993.Google Scholar
[14]D., Pilaud, P., Caspi, N., Halbwachs and J., Plaice. Lustre: a declarative language for programming synchronous systems. In 14th ACM Conference on Principles of Programming Languages, pp. 178–188, Munich, January 1987.Google Scholar
,The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.1, July 2006. http://coq.inria.fr.

Save book to Kindle

To save this book to your Kindle, first ensure [email protected] is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the ‘name’ part of your Kindle email address below. Find out more about saving to your Kindle.

Note you can select to save to either the @free.kindle.com or @kindle.com variations. ‘@free.kindle.com’ emails are free but can only be saved to your device when it is connected to wi-fi. ‘@kindle.com’ emails can be delivered even when you are not connected to wi-fi, but note that service fees apply.

Find out more about the Kindle Personal Document Service.

Available formats
×

Save book to Dropbox

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Dropbox.

Available formats
×

Save book to Google Drive

To save content items to your account, please confirm that you agree to abide by our usage policies. If this is the first time you use this feature, you will be asked to authorise Cambridge Core to connect with your account. Find out more about saving content to Google Drive.

Available formats
×