Skip to main content
SpringerLink
Log in

Partial Evaluation and Non-interference for Object Calculi

  • Conference paper
Functional and Logic Programming (FLOPS 1999)

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

Included in the following conference series:

Abstract

We prove the correctness of a multi-level partial evaluator and of an information flow analysis for Abadi and Cardelli’s FOb 1 ≤ :, a simply typed object calculus with function and object types, object subtyping and subsumption.

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. Abadi, M.: Secrecy by typing in security protocols. Journal of the ACM (to appear)

    Google Scholar 

  2. Abadi, M., Banerjee, A., Heintze, N., Riecke, J.: A core calculus of dependency. In: Proceedings of POPL 1999, pp. 147–160. ACM Press, New York (1999)

    Google Scholar 

  3. Abadi, M., Cardelli, L.: A theory of objects. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  4. Bell, D., LaPadula, L.: Secure computer systems: Unified exposition and multics interpretation. Technical Report MTR-2997, MITRE Corporation (July 1975)

    Google Scholar 

  5. Bertino, E., Ferrari, E., Samarati, P.: Mandatory security and object-oriented systems: A multilevel entity model and its mapping onto a single-level object model. Theory and Practice of Object Systems 4(3), 183–204 (1998)

    Article  Google Scholar 

  6. Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings. Information and Computation (1999); To appear in a special issue with papers from Theoretical Aspects of Computer Software (TACS)

    Google Scholar 

  7. Consel, C., Hornof, L., Marlet, R., Muller, G., Thibault, S., Volanschi, E.-N.: Tempo: Specializing systems applications and beyond. ACM Computing Surveys  30(3) (September 1998); Symposium on Partial Evaluation (SOPE 1998)

    Google Scholar 

  8. Danvy, O., Glück, R., Thiemann, P. (eds.): Partial Evaluation 1996. LNCS, vol. 1110. Springer, Heidelberg (1996)

    Google Scholar 

  9. Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19(5), 236–243 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  10. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)

    Article  MATH  Google Scholar 

  11. Glück, R., Jørgensen, J.: An automatic program generator for multi-level specialization. Lisp and Symbolic Computation 10(2), 113–158 (1997)

    Article  Google Scholar 

  12. Gordon, A.D., Hankin, P.D., Lassen, S.B.: Compilation and equivalence of imperative objects. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 74–87. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Gordon, A.D., Rees, G.D.: Bisimilarity for a first-order calculus of objects with subtyping. In: Proceedings of POPL 1996, pp. 386–395. ACM Press, New York (1996)

    Chapter  Google Scholar 

  14. Hatcliff, J., Glück, R.: Reasoning about hierarchies of online program specialization systems. In: Danvy, O., et al. (eds.) [8], pp. 161–182.

    Google Scholar 

  15. Heintze, N., Riecke, J.: The SLam calculus: programming with secrecy and integrity. In: Proceedings of POPL 1998, pp. 365–377. ACM Press, New York (1998)

    Chapter  Google Scholar 

  16. Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

  17. Marquard, M., Steensgaard, B.: Partial evaluation of an object-oriented language. Master’s thesis, Department of Computer Science, Copenhagen University, DIKU (1992)

    Google Scholar 

  18. Myers, A.C.: Jflow: Practical mostly-static information flow control. In: Proceedings of POPL 1999, pp. 228–241. ACM Press, New York (1999)

    Google Scholar 

  19. Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: Proceedings of SOSP 1997, pp. 129–142. ACM Press, New York (1997)

    Chapter  Google Scholar 

  20. Nielson, F., Nielson, H.R.: Two-level functional languages. Cambridge Tracts In Theoretical Computer Science, vol. 34. Cambridge University Press, Cambridge (1992)

    Book  MATH  Google Scholar 

  21. Nielson, F., Nielson, H.R.: Multi-level lambda-calculi: an algebraic description. In: Danvy, O., et al. (eds.) [8], pp. 338–354.

    Google Scholar 

  22. Nielson, F., Nielson, H.R.: Flow analyis for imperative objects. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 220–228. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  23. Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 40–58. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Sangiorgi, D.: An interpretation of typed objects into typed π-calculus. Information and Computation 143(1), 34–73 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  25. Schultz, U.P., Lawall, J., Consel, C., Muller, G.: Toward Automatic Specialization of Java Programs. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 367–390. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  26. Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of POPL 1998, pp. 355–364. ACM Press, New York (1998)

    Chapter  Google Scholar 

  27. Thiemann, P.: A unified framework for binding-time analysis. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214. Springer, Heidelberg (1997)

    Google Scholar 

  28. Thiemann, P., Klaeren, H.: What security analysis can do for you or the correctness of a multi-level binding-time analysis. Manuscript (June 1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, France

    Gilles Barthe & Bernard P. Serpette

  2. Departamento de Informática, Universidade do Minho, Portugal

    Gilles Barthe

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernard P. Serpette
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Aart Middeldorp

  2. Tokyo Institute of Technology, Graduate School of Information Sciences and Engineering Ookayama, 2-12-2, Meguro-ku, 152-8552, Tokyo, Japan

    Taisuke Sato

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Serpette, B.P. (1999). Partial Evaluation and Non-interference for Object Calculi. In: Middeldorp, A., Sato, T. (eds) Functional and Logic Programming. FLOPS 1999. Lecture Notes in Computer Science, vol 1722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10705424_4

Download citation

  • DOI: https://doi.org/10.1007/10705424_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66677-6

  • Online ISBN: 978-3-540-47950-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation