Skip to main content
SpringerLink
Log in

An Automata-Theoretic Model of Idealized Algol

(Extended Abstract)

  • Conference paper
Automata, Languages, and Programming (ICALP 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7392))

Included in the following conference series:

Abstract

In this paper, we present a new model of class-based Algol-like programming languages inspired by automata-theoretic concepts. The model may be seen as a variant of the ”object-based” model previously proposed by Reddy, where objects are described by their observable behaviour in terms of events. At the same time, it also reflects the intuitions behind state-based models studied by Reynolds, Oles, Tennent and O’Hearn where the effect of commands is described by state transformations. The idea is to view stores as automata, capturing not only their states but also the allowed state transformations. In this fashion, we are able to combine both the state-based and event-based views of objects. We illustrate the efficacy of the model by proving several test equivalences and discuss its connections to the previous models.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: LICS 1998, pp. 334–344 (1998)

    Google Scholar 

  2. Abramsky, S., McCusker, G.: Linearity, sharing and state. In: Algol-like Languages [16], ch. 20

    Google Scholar 

  3. Barnett, M., Naumann, D.A.: Friends Need a Bit More: Maintaining Invariants Over Shared State. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 54–84. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-Guarantee Reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363–377. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: ICFP (2010)

    Google Scholar 

  6. Dunphy, B.P., Reddy, U.S.: Parametric limits. In: LICS, pp. 242–253. IEEE (July 2004)

    Google Scholar 

  7. Eilenberg, S.: Automata, Languages, and Machines, vol. A and B. Academic Press (1974)

    Google Scholar 

  8. Fiore, M.P., Jung, A., Moggi, E., O’Hearn, P.W., Riecke, J., Rosolini, G., Stark, I.: Domains and denotational semantics: History, accomplishments and open problems. EATCS 59, 227–256 (1996)

    Google Scholar 

  9. Rustan, K., Leino, M., Schulte, W.: Using History Invariants to Verify Observers. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 80–94. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables. In: POPL, pp. 191–203. ACM (1988); Reprinted as Chapter 7 of [16]

    Google Scholar 

  11. Mitchell, J.C., Plotkin, G.D.: Abstract types have existential types. TOPLAS 10(3), 470–502 (1988)

    Article  Google Scholar 

  12. O’Hearn, P.W., Reddy, U.S.: Objects, interference and the Yoneda embedding. Theoretical Computer Science 228(1), 211–252 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  13. O’Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambda-calculus. JACM 47(1), 167–223 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  14. O’Hearn, P.W., Tennent, R.D.: Semantical analysis of specification logic, Part 2. Inf. Comput. 107(1), 25–57 (1993); Reprinted as Chapter 14 of [16]

    Article  MathSciNet  MATH  Google Scholar 

  15. O’Hearn, P.W., Tennent, R.D.: Parametricity and local variables. JACM 42(3), 658–709 (1995); Reprinted as Chapter 16 of [16]

    Article  MathSciNet  MATH  Google Scholar 

  16. O’Hearn, P.W., Tennent, R.D.: Algol-like Languages, vol. 2. Birkhäuser, Boston (1997)

    Google Scholar 

  17. Oles, F.J.: Type algebras, functor categories and block structure. In: Nivat, M., Reynolds, J.C. (eds.) Algebraic Methods in Semantics, pp. 543–573. Cambridge Univ. Press (1985)

    Google Scholar 

  18. Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Gordon, A.M., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, pp. 227–274. Cambridge Univ. Press, Cambridge (1998)

    Google Scholar 

  19. Reddy, U.S.: Global state considered unnecessary: An introduction to object-based semantics. J. Lisp and Symbolic Computation 9, 7–76 (1996); Reprinted as Chapter 19 of [16]

    Article  Google Scholar 

  20. Reddy, U.S.: Parametricity and naturality in the semantics of Algol-like languages. Electronic manuscript, University of Birmingham (December 1998), http://www.cs.bham.ac.uk/~udr/

  21. Reddy, U.S.: Objects and classes in Algol-like languages. Inf. Comput. 172, 63–97 (2002)

    Article  MATH  Google Scholar 

  22. Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Sci. of Comput. Prog. 50(1-3), 129–160 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  23. Reynolds, J.C.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages, pp. 345–372. North-Holland (1981); Reprinted as Chapter 3 of [16]

    Google Scholar 

  24. Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A. (ed.) Information Processing 1983, pp. 513–523. North-Holland, Amsterdam (1983)

    Google Scholar 

  25. Tennent, R.D.: Denotational semantics. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 169–322. Oxford University Press (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Birmingham, UK

    Uday S. Reddy

  2. University of Illinois at Urbana-Champaign, USA

    Brian P. Dunphy

Authors
  1. Uday S. Reddy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Brian P. Dunphy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Centre for Discrete Mathematics and its Applications, University of Warwick, Warwick, UK

    Artur Czumaj

  2. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Kurt Mehlhorn

  3. Computer Laboratory,, University of Cambridge, UK

    Andrew Pitts

  4. ETH Zurich, Switzerland

    Roger Wattenhofer

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reddy, U.S., Dunphy, B.P. (2012). An Automata-Theoretic Model of Idealized Algol. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds) Automata, Languages, and Programming. ICALP 2012. Lecture Notes in Computer Science, vol 7392. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31585-5_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31585-5_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31584-8

  • Online ISBN: 978-3-642-31585-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation