Skip to main content

Completude d'un systeme formel pour prouver l'equivalence de certains schemas recursifs monadiques

  • Schemas De Programmes Schematology
  • Conference paper
  • First Online:
Programming Symposium

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 19))

  • 2067 Accesses

Résumé

Dans [3] de Bakker et Scott définissent une classe de schémas de programmes et un système formel permettant de prouver certaines propriétés de ces schémas. Sous le nom de μ-calculus, ce système a été repris par de Bakker [2] qui a montré que le système est complet relativement aux formules exprimant l'équivalence des schémas de Ianov. Nous montrons ici la complétude de ce système pour les schémas récursifs monadiques définis par Ashcroft, Manna et Pnueli [1] (et écrits sans la fonction identité).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Références

  1. E. Ashcroft, Z. Manna, A. Pnueli "Decidable Properties of Monadic Functional Schemes" in Theory of Machines and Computations (Eds: Kohavi and Paz), New York 1971, 3–17.

    Google Scholar 

  2. J.W. de Bakker "Recursive Procedures", Mathematical Center Tract n o 24, Amsterdam 1971.

    Google Scholar 

  3. J.W. de Bakker, D. Scott "A Theory of Programs", 1969, Unpublished.

    Google Scholar 

  4. B. Courcelle "Grammaires canoniques des Langages simples", Revue de l'Association pour l'Informatique et la Recherche Opérationnelle, 1974, no1.

    Google Scholar 

  5. F.G. Cousineau, J.M. Rifflet "Schémas de Programme: Problèmes d'Equivalence et Complexité", Thèse de 3ème cycle, Paris 1974.

    Google Scholar 

  6. P. Hitchcok, D. Park "Induction Rules and Termination Proofs" Automata, Languages and Programming pp 225–252, 1973. (Colloque IRIA 1972).

    Google Scholar 

  7. J.E. Hopcroft, A.J. Korenjak "Simple Deterministic Languages", IEEE 7th Annual Symposium on Switching and Automata Theory pp 36–46.

    Google Scholar 

  8. D. Luckham, D. Park, M. Paterson "On Formalized Computer Programs" J.C.S.S. vol 4, pp 220–249.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

B. Robinet

Rights and permissions

Reprints and permissions

Copyright information

© 1974 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Courcelle, B., Vuillemin, J. (1974). Completude d'un systeme formel pour prouver l'equivalence de certains schemas recursifs monadiques. In: Robinet, B. (eds) Programming Symposium. Lecture Notes in Computer Science, vol 19. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-06859-7_137

Download citation

  • DOI: https://doi.org/10.1007/3-540-06859-7_137

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-06859-4

  • Online ISBN: 978-3-540-37819-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics