Abstract
Kahn and MacQueen [13, 14] proposed considering a parallel dataflow program as a network of functional transformers over infinite lists (also called streams). Recently, type theory and the “proofs as programs” paradigm have proved useful for the validation of functional programs.
We propose to relate both approaches, by studying a special dataflow program (the Sieve of Eratosthenes) in two strongly-typed lambda-calculi (system F and the Calculus of Constructions).
The originality of our approach is the introduction of a type of parameterized streams which uses the mechanism of dependent types in the Calculus of Constructions. The Sieve of Eratosthenes consists of an infinite list which gives both the integer and the proof that it is the first prime since the last output.
This research started during F. Leclerc's DEA project at LIP (spring 91). It was partly supported by ESPRIT Basic Research Actions “Logical Frameworks” and “Types for Proofs and Programs” and by MRE Programme de Recherches Coordonnées and CNRS GDR “Programmation”.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Boerio. Extending pruning techniques to polymorphic second order λ-calculus. In Proceedings ESOP'94, 1994.
C. Böhm and A. Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39, 1985.
R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
Th. Coquand. Infinite objects in type theory. In [10], 1993.
Th. Coquand and G. Huet. Constructions: A higher order proof system for mechanizing mathematics. In EUROCAL'85, Linz, 1985. Springer-Verlag. LNCS 203.
Th. Coquand and G. Huet. Concepts mathématiques et informatiques formalisés dans le calcul des constructions. In The Paris Logic Group, editor, Logic Colloquium'85. North-Holland, 1987.
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User's Guide Version 5.8. Rapport Technique 154, INRIA, May 1993.
P. Dybjer and H. Sander. A functional programming approach to the specification and verification of concurrent systemsnd verification of concurrent systems. Formal Aspects of Computing, 1:303–318, 1989.
H. Geuvers. Inductive and coinductive types with iteration and recursion. Faculty of Mathematics and Informatics, Catholic University Nijmegen, 1991.
H. Geuvers, editor. Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, 1993.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.
S. Hayashi. Singleton, union, intersection types for program extraction. In Proceedings of TACS'91, 1991.
G. Kahn. The semantics of a simple language for parallel programming. In Information Processing 74. North-Holland, 1974.
G. Kahn and D. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing 77. North-Holland, 1977.
L.C. Paulson. Co-induction and co-recursion in higher-order logic. available by anonymous ftp.
N. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, 1988.
N. Mendler. Predicative types universes and primitive recursion. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 173–184. Amsterdam, The Netherlands, IEEE Computer Society Press, 1991.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory.International Series of Monographs on Computer Science. Oxford Science Publications, 1990.
C. Parent. Developing certified programs in the system Coq-The Program tactic. Technical Report 93-29, Ecole Normale Supérieure de Lyon, October 1993. also in Proceedings of the BRA Workshop Types for Proofs and Programs, may 93.
M. Parigot, P. Manoury, and M. Simonot. Propre: A programming language with proofs. In A. Voronkov, editor, Logic Programming and automated reasoning, number 624 in LNCS, St. Petersburg, Russia, July 1992. Springer-Verlag.
C. Paulin-Mohring. Extracting Fω's programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM.
C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Université Paris 7, January 1989.
Ch. Raffalli. L'arithmétique fonctionnelle du second ordre avec points fixes. PhD thesis, Université Paris VII, 1994.
G. C. Wraith. A note on categorical data types. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Category Theory and Computer Science. Springer-Verlag, 1989. LNCS 389.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leclerc, F., Paulin-Mohring, C. (1994). Programming with streams in Coq a case study: The Sieve of Eratosthenes. In: Barendregt, H., Nipkow, T. (eds) Types for Proofs and Programs. TYPES 1993. Lecture Notes in Computer Science, vol 806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58085-9_77
Download citation
DOI: https://doi.org/10.1007/3-540-58085-9_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58085-0
Online ISBN: 978-3-540-48440-0
eBook Packages: Springer Book Archive