Semantics and axiomatics of a simple recursive language.

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Semantics and axiomatics of a simple recursive language.

Full text

Pdf (661 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the sixth annual ACM symposium on Theory of computing table of contents

Seattle, Washington, United States

Pages: 13 - 26

Year of Publication: 1974

Authors

B. Courcelle
J. Vuillemin

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 16, Citation Count: 5

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/800119.803880 What is a DOI?

ABSTRACT

In this paper, we provide a simple recursive programming language with a semantics and a formal proof system, along the lines of [5], [17] and [23]. We show that the semantics used is the “best” possible if one admits the validity of Algol's copy rule, and that the proof system is complete with respect to the semantics. The definitions and methods used are meant to provide a basis for a broader theory of program schemas, which models parallel as well as sequential programs.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	E.A. Ashcroft, Z. Manna, "Formalization of Properties of Parallel Program" Memo Stanford AIM 110 (1970).
	2	E.A. Ashcroft, Z. Manna, A. Pnueli, "Decidable Properties of Monadic Functional Schemas" in Theory of Machines and Computations Kohavi and Paz, Eds. Academic Press, pp. 3-18 (1971).
	3	J.W. de Bakker, "Recursive Procedures", Mathematical Center Tracts n ° 24, Amsterdam. (1971).
	4	J.W. de Bakker, W.P. de Roever, "A Calculus for Recursive Program Schemes", Proceedings of IRIA Colloquium, North-Holland (1972).
	5	J.W. de Bakker, D. Scott, "A Theory of Programs", unpublished (1969).
	6	B. Courcelle, "Grammaires Canoniques des Langages Simples Déterministes", RAIRO n° 1 Paris (1974).
	7	B. Courcelle, G. Kahn, J.Vuillemin, "Algorithmes d'Equivalence pour des Equations Récursives Simples", Rapport Laboria no 37, IRIA, (1973).
	8	B. Courcelle, J. Vuillemin, "Complétude d'un Système Formel pour l'Equivalence de Certains Schémas Récursifs Monadiques", To appear in Compte-rendu du Collogue de Paris (Avril 1974).
	9	M. Gordon, "Evaluation and Denotation of pure LISP Programs: a Worked Example in Semantics", Thesis, Edinburgh (1973).
	10	M.S. Paterson, C. Hewitt, "Comparative Schematology", in Record of Project MAC Conference on Parallel Computation, ACM, New York (1970).
	11	P. Hitchcock, D. Park, "Induction Rules and Proofs of Termination" Proceedings of IRIA Colloquium, North Holland (1972).
	12	J.E. Hopcroft, A.J. Korenjak, "Simple Deterministic Languages", 7th SWAT (1966), pp. 36-46.
	13	Y.I. Ianov, "The Logical Schemes of Algorithms", Problems in Cybernetics, vol. 1, Pergamon Press. (1960).
	14	G. Kahn, "A Preliminary Theory of Parallel Programs", Rapport Laboria n° 6, IRIA (1973).
	15	D. Luckham, D. Park, M.S. Paterson, "On Formalized Computer Programs", JCSS vol. 4, n° 3, pp. 220-249, (1970).
	16	Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
	17	Robin Milner, Models of LCF., Stanford University, Stanford, CA, 1973
	18	R. Milner, "Processes: a model of computing agents", University of Edinburgh. Unpublished memo. (1973).
	19	R. Milner, R. Weyrauch, "Proving Compiler Correctness in a Mechanized Logic", Machine Intelligence 7, Edinburgh University Press. (1972).
	20	M. Nivat, "Sur l'Interprétation des Schémas de Programmes Monadiques", Rapport Laboria n° 1, IRIA (1972).
	21	M. Newey, Ph.D. thesis, Computer Science Department, Stanford (1973).
	22	M. Paterson, "Program Schemata", in MI 3, Edinburgh University (1968).
	23	D. Scott, "Outline of a Mathematical Theory of Computation", Oxford mono., PRG-2, Oxford University (1970).
	24	D. Scott "Continuous Lattices", Oxford mon. PRG-7 (1972).
	25	D. Scott, C. Strachey, "Towards a Mathematical Semantics for Computer Languages", Oxford mono., PRG-6, Oxford University (1972).
	26	Jean Etienne Vuillemin, Proof-techniques for recursive programs., 1974
	27	Jean Vuillemin, Correct and optimal implementations of recursion in a simple programming language, Proceedings of the fifth annual ACM symposium on Theory of computing, p.224-239, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804054]
	28	J. Vuillemin, "Syntaxe, Sémantique et Axiomatique d'un Langage de Programmation Simple", Thèse d'Etat (To appear).

CITED BY 5

	R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977
	J. A. Goguen , J. W. Thatcher , E. G. Wagner , J. B. Wright, Initial Algebra Semantics and Continuous Algebras, Journal of the ACM (JACM), v.24 n.1, p.68-95, Jan. 1977
	R. M. Burstall , John Darlington, Some transformations for developing recursive programs, ACM SIGPLAN Notices, v.10 n.6, p.465-472, June 1975
	M. C.B. Hennessy , E. A. Ashcroft, Parameter-passing mechanisms and nondeterminism, Proceedings of the ninth annual ACM symposium on Theory of computing, p.306-311, May 04-04, 1977, Boulder, Colorado, United States
	H. P. Künzi , M. P. Schellekens, On the Yoneda completion of a quasi-metric space, Theoretical Computer Science, v.278 n.1-2, p.159-194, May 6, 2002