Skip to main content
SpringerLink
Log in

Sequential functions on indexed domains and full abstraction for a sub-language of PCF

  • Conference paper
  • First Online:
Mathematical Foundations of Programming Semantics (MFPS 1993)

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

  • 152 Accesses

Abstract

We present a general semantic framework of sequential functions on domains equipped with a parameterized notion of incremental sequential computation. Under the simplifying assumption that computation over function spaces proceeds by successive application to constants, we construct a sequential semantic model for a non-trivial sublanguage of PCF with a corresponding syntactic restriction — that variables of function type may only be applied to closed terms. We show that the model is fully abstract for the sub-language, with respect to the usual notion of program behavior.

This research was supported in part by National Science Foundation grant CCR-9006064.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Berry and P.-L. Curien. Sequential algorithms on concrete data structures. Theoretical Computer Science, 20:265–321, 1982.

    Google Scholar 

  2. G. Berry and P.-L. Curien. Theory and practice of sequential algorithms: the kernel of the applicative language CD80. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 2, pages 35–87. Cambridge University Press, 1985.

    Google Scholar 

  3. G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 3, pages 89–132. Cambridge University Press, 1985.

    Google Scholar 

  4. A. Bucciarelli and T. Ehrhard. Sequentiality and strong stability. In Proc. Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, July 1991.

    Google Scholar 

  5. G. Berry. Stable models of typed λ-calculi. In Proc. 5 th Coll. on Automata, Languages and Programming, number 62 in Lecture Notes in Computer Science, pages 72–89. Springer-Verlag, July 1978.

    Google Scholar 

  6. S. Brookes and S. Geva. Stable and sequential functions on Scott domains. Technical Report CMU-CS-92-121, School of Computer Science, Carnegie Mellon University, June 1992.

    Google Scholar 

  7. R. Cartwright and M. Felleisen. Observable sequentiality and full abstraction. In Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 328–342. ACM Press, January 1992.

    Google Scholar 

  8. P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Research Notes in Theoretical Computer Science. Pitman, 1986. Second edition, expanded and updated, published by Birkhäuser, Boston, 1993.

    Google Scholar 

  9. P.-L. Curien. Observable algorithms on concrete data structures. In Seventh Annual IEEE Symposium on Logic in Computer Science, pages 432–443. IEEE Computer Society Press, June 1992.

    Google Scholar 

  10. G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer Verlag, 1980.

    Google Scholar 

  11. G. Kahn and G. D. Plotkin. Domaines concrets. Rapport 336, IRIA-LABORIA, 1978. English translation (with historical introduction by S. Brookes) to appear in Theoretical Computer Science, 1993.

    Google Scholar 

  12. R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1–22, 1977.

    Google Scholar 

  13. K. Mulmuley. Full Abstraction and Semantic Equivalence. MIT Press, 1987.

    Google Scholar 

  14. G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–255, 1977.

    Google Scholar 

  15. V. Yu. Sazonov. Sequentially and parallelly computable functional. In Proc. Symp. on Lambda-Calculus and Computer Science Theory, number 37 in Lecture Notes in Computer Science. Springer-Verlag, 1975.

    Google Scholar 

  16. A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Pitman, 1988.

    Google Scholar 

  17. J. Vuillemin. Proof techniques for recursive programs. PhD thesis, Stanford University, 1973.

    Google Scholar 

  18. G. Q. Zhang. Logic of Domains. Progress in Theoretical Computer Science. Birkhäuser, Boston, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, 15213, Pittsburgh, PA

    Stephen Brookes & Shai Geva

Authors
  1. Stephen Brookes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shai Geva
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stephen Brookes Michael Main Austin Melton Michael Mislove David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brookes, S., Geva, S. (1994). Sequential functions on indexed domains and full abstraction for a sub-language of PCF. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-58027-1_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58027-0

  • Online ISBN: 978-3-540-48419-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation