Skip to main content
SpringerLink
Log in

MetaKlaim: Meta-programming for Global Computing

Position Paper

  • Conference paper
  • First Online:
Semantics, Applications, and Implementation of Program Generation (SAIG 2001)

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

Abstract

Most foundational models for global computing have focused on the spatial dimension of computations, however global computing requires also new ways of thinking about the temporal dimension. In particular, withno central control and the need to operate with incomplete information there is a compelling need to interleave meta-programming activities (like assembly and linking of code fragments), security checks (like type-checking at administrative boundaries) and normal computational activities. MetaKlaim is a case study in modeling both spatial and temporal aspects of computing by integrating MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility). The staging annotations of MetaML provide a fine-grain control of the temporal aspects, while Klaim allows to model and program the spatial aspects of distributed concurrent applications. Our approachfor combining these aspects is quite general and should be applicable to other languages/systems for network programming.

Work supported by APPSEM WG and MURST projects SALADIN and TOSCA.

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. C. Calcagno, E. Moggi, T. Sheard, W. Taha. Closed types for safe imperative MetaML. submitted for publication, 2001.

    Google Scholar 

  2. L. Cardelli. Program Fragments, Linking, and Modularization. In Proc. of the ACM Symposium on Principles of Programming Languages, ACM Press, 1997.

    Google Scholar 

  3. L. Cardelli and A. Gordon. Mobile Ambients. Theoretical Computers Science 240 (1), Elsevier 2000.

    Google Scholar 

  4. L. Cardelli, A. Gordon. Types for Mobile Ambients. In Proc. of the ACM Symposium on Principles of Programming Languages, pp.79–92, ACM Press, 1999.

    Google Scholar 

  5. L. Cardelli, Abstractions for Mobile Computing, In In Secure Internet Programming: Se curity Issues for Distributed and Mobile Objects (J. Vitek, C. Jensen, Eds.), LNCS State-Of-The-Art-Survey, LNCS 1603, Springer, 1999.

    Google Scholar 

  6. N. Carriero, D. Gelernter. Linda in Context. Communications of the ACM, 32W(4):444–458, ACM Press, 1989.

    Article  Google Scholar 

  7. R. Davies. A temporal-logic approachto binding-time analysis. In 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 184–195, New Brunswick, 1996. IEEE Computer Society Press.

    Google Scholar 

  8. R. Davies, F. Pfenning. A modal analysis of staged computation. In 23rd Annual ACM Symposium on Principles of Programming Languages (POPL), pages 258–270, St. Petersburg Beach, 1996.

    Google Scholar 

  9. R. De Nicola, G. L. Ferrari, R. Pugliese. KLAIM: A Kernel Language for Agents Interaction and Mobility, IEEE Transactions on Software Engineering, 24(5):315–330, IEEE Computer Society, 1998.

    Article  Google Scholar 

  10. R. De Nicola, G. L. Ferrari, R. Pugliese. Types as Specifications of Access Policies. In In Secure Internet Programming:Se curity Issues for Distributed and Mobile Objects (J. Vitek, C. Jensen, Eds.), LNCS State-Of-The-Art-Survey, LNCS 1603, Springer, pp.117–146, 1999.

    Google Scholar 

  11. R. De Nicola, G. Ferrari, R. Pugliese. Programming Acess Control: The KLAIM Experience, In Proc. CONCUR‘2000, LNCS 1877, 2000.

    Google Scholar 

  12. R. De Nicola, G. L. Ferrari, R. Pugliese, B. Venneri. Types for Access Control. Theoretical Computers Science, 240(1):215–254, special issue on Coordination, Elsevier Science, July 2000.

    Google Scholar 

  13. S. Drossopoulou. Towards an Abstract Model of Java Dynamic Linking and Verification. In Proc. Types in Compilation, 2000.

    Google Scholar 

  14. S. Drossopoulou, S. Eisenbach, D. Wragg. A fragment calculus-towards a model of separate compilation, linking and binary compatibility. In 14th Symposium on Logic in Computer Science (LICS‘99), pages 147–156, Washington-Brussels-Tokyo, July 1999. IEEE.

    Google Scholar 

  15. G. Ferrari, E. Moggi, R. Pugliese. Global Types and Network Services. In Proc. ConCoord:International Workshop on Concurrency and Coordination, ENTCS 54 (Montanari and Sassone Eds), Elsevier Science, 2001.

    Google Scholar 

  16. A. Fuggetta, G. Picco, G. Vigna. Understanging Code Mobility, IEEE Transactions on Software Engineering, 24(5), IEEE Computer Society, 1998.

    Google Scholar 

  17. Fournet, C., Gonthier, G. Levy, J-J., Maranget, L., Remy, D. A Calculus of Mobile Agents, In Proc. CONCUR‘96, LNCS 1119, Springer, 1996.

    Google Scholar 

  18. J-Y. Girard. Interprétation fonctionelle et élimination des coupures de l‘arithmétique d‘ordre supérieur. PhD. Thesis, Université Paris VII, 1972.

    Google Scholar 

  19. D. Gelernter. Generative Communication in Linda. ACM Transactions on Programming Languages and Systems, 7(1):80–112, ACM Press, 1985.

    Article  MATH  Google Scholar 

  20. R. Gray, D. Kotz, G. Cybenko and D. Rus. D‘Agents: Security in a multiplelanguage, mobile-agent system. In G. Vigna, editor, Mobile Agents and Security, Lecture Notes in Computer Science, Springer-Verlag, 1998.

    Google Scholar 

  21. M. Hennessy, J. Riely. Distributed Processes and Location Failures, Theoretical Computers Science, to appear, 2001.

    Google Scholar 

  22. M. Hennessy, J. Riely. Resource Access Control in Systems of Mobile Agents, Information and Computation, to appear, 2001.

    Google Scholar 

  23. M. Hicks and S. Weirich. A Calculus for Dynamic Loading, Technical report, MSCIS-00-07, University of Pennsylvania, 2000, (available on line http://www.cis.upenn.edu/mwh/papers/loadcalc.pdf).

  24. S. Kamin, M. Callahan, L. Clausen. Lightweight and generative components II: Binary-level components. In [31], pages 28–50, 2000.

    Google Scholar 

  25. The MetaML Home Page provides source code and online documentation http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html.

  26. E. Moggi, W. Taha, Z. Benaissa, T. Sheard. An idealized MetaML: Simpler, and more expressive. In European Symposium on Programming (ESOP), volume 1576 of Lecture Notes in Computer Science, pages 193–207. Springer-Verlag, 1999.

    Google Scholar 

  27. F. Nielson, H. R. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.

    Google Scholar 

  28. Z. Qian, A. Goldberg, A. Coglio. A formal specification of JavaTM class loading. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Application (OOPSLA-00), volume 35.10 of ACM Sigplan Notices, pages 325–336, N. Y., October 15–19 2000. ACM Press.

    Google Scholar 

  29. P. Sewell. Modules, Abstract Types and Distributed Versioning. In Proc. ACM Symposium on Principles of Programming Languages, ACM Press, 2001.

    Google Scholar 

  30. P. Sewell, P. Wojciechowski. Nomadic Pict: Language and Infrastructure Design for Mobile Agents. IEEE Concurrency, 2000.

    Google Scholar 

  31. W. Taha, editor. Semantics, Applications, and Implementation of Program Generation, volume 1924 of Lecture Notes in Computer Science, Montréal, 2000. Springer-Verlag.

    MATH  Google Scholar 

  32. J.-P. Talpin, P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  33. J.-P. Talpin, P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245–296, June 1994.

    Article  MATH  MathSciNet  Google Scholar 

  34. J. Vitek, G. Castagna. Towards a Calculus of Secure Mobile Computations. In Workshop on Internet Programming Languages, LNCS 1686, Springer, 1999.

    Google Scholar 

  35. A.K. Wright, M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1), 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dip. di Informatica, Univ. di Pisa, Italy

    Gianluigi Ferrari

  2. Dip. di Informatica e Scienze dell’Informazione, Univ. di Genova, Italy

    Eugenio Moggi

  3. Dip. di Sistemi e Informatica, Univ. di Firenze, Italy

    Rosario Pugliese

Authors
  1. Gianluigi Ferrari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenio Moggi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rosario Pugliese
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Yale University, 51 Prospect St., New Haven, CT, 06511, USA

    Walid Taha

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ferrari, G., Moggi, E., Pugliese, R. (2001). MetaKlaim: Meta-programming for Global Computing. In: Taha, W. (eds) Semantics, Applications, and Implementation of Program Generation. SAIG 2001. Lecture Notes in Computer Science, vol 2196. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44806-3_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-44806-3_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42558-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation