Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Berger, Martin; Tratt, Laurence (2010)
Languages: English
Types: Unknown

Classified by OpenAIRE into

A meta-program is a program that generates or manipulates another program; in homogeneous meta-programming, a program may generate new parts of, or manipulate, itself. Meta-programming has been used extensively since macros\ud were introduced to Lisp, yet we have little idea how formally to reason about metaprograms. This paper provides the first program logics for homogeneous metaprogramming\ud – using a variant of MiniMLe by Davies and Pfenning as underlying meta-programming language.We show the applicability of our approach by reasoning about example meta-programs from the literature. We also demonstrate that our logics are relatively complete in the sense of Cook, enable the inductive derivation of characteristic formulae, and exactly capture the observational properties induced by the operational semantics.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. M. Berger. Program Logics for Sequential Higher-Order Control. In Proc. FSEN, pages 194- 211, 2009.
    • 2. M. Berger, K. Honda, and N. Yoshida. A Logical Analysis of Aliasing in Imperative HigherOrder Functions. J. Funct. Program., 17(4-5):473-546, 2007.
    • 3. M. Berger, K. Honda, and N. Yoshida. Completeness and logical full abstraction in modal logics for typed mobile processes. In Proc. ICALP, pages 99-111, 2008.
    • 4. M. Berger and L. Tratt. Program Logics for Homogeneous Metaprogramming. Long version of the present paper, to appear.
    • 5. S. A. Cook. Soundness and completeness of an axiom system for program verification. SIAM J. Comput., 7(1):70-90, 1978.
    • 6. R. Davies and F. Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001.
    • 7. S. Fogarty, E. Pasˇalic´, J. Siek, and W. Taha. Concoqtion: Indexed Types Now! In Proc. PEPM, pages 112-121, 2007.
    • 8. C. A. Gunter. Semantics of Programming Languages. MIT Press, 1995.
    • 9. K. Honda. From Process Logic to Program Logic. In ICFP'04, pages 163-174. ACM Press, 2004.
    • 10. K. Honda, M. Berger, and N. Yoshida. Descriptive and Relative Completeness of Logics for Higher-Order Functions. In Proc. ICALP, pages 360-371, 2006.
    • 11. K. Honda and N. Yoshida. A compositional logic for polymorphic higher-order functions. In Proc. PPDP, pages 191-202, 2004.
    • 12. K. Honda, N. Yoshida, and M. Berger. An Observationally Complete Program Logic for Imperative Higher-Order Functions. In LICS'05, pages 270-279, 2005.
    • 13. J. Longley and G. Plotkin. Logical Full Abstraction and PCF. In Tbilisi Symposium on Logic, Language and Information, CSLI, 1998.
    • 14. J. C. Reynolds. Separation logic: a logic for shared mutable data structures. In Proc. LICS'02, pages 55-74, 2002.
    • 15. T. Sheard and N. Linger. Programming in Wmega. In Proc. Central European Functional Programming School, pages 158-227, 2007.
    • 16. T. Sheard and S. Peyton Jones. Template meta-programming for Haskell. In Proc. Haskell Workshop, pages 1-16, 2002.
    • 17. W. Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1993.
    • 18. W. Taha and M. F. Nielsen. Environment classifiers. In Proc. POPL, pages 26-37, 2003.
    • 19. L. Tratt. Compile-time meta-programming in a dynamically typed OO language. In Proc. DLS, pages 49-64, Oct. 2005.
    • 20. E. Westbrook, M. Ricken, J. Inoue, Y. Yao, T. Abdelatif, and W. Taha. Mint: Java multi-stage programming using weak separability. In Proc. PLDI, 2010. To appear.
    • 21. N. Yoshida, K. Honda, and M. Berger. Logical reasoning for higher-order functions with local state. In Proc. Fossacs, LNCS, pages 361-377, 2007.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article