Berger, Martin and Tratt, Laurence (2010) Program logics for homogeneous meta-programming. In: Clarke, E M and Voronkov, A (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science, 6355 L . Springer Verlag, pp. 64-81. ISBN 3642175104
![]() |
PDF
Restricted to SRO admin only Download (188kB) |
Abstract
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 were introduced to Lisp, yet we have little idea how formally to reason about meta-programs. This paper provides the first program logics for homogeneous meta-programming - using a variant of MiniML 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.
Item Type: | Book Section |
---|---|
Additional Information: | Proceedings 16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010 |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Depositing User: | Martin Berger |
Date Deposited: | 06 Feb 2012 21:27 |
Last Modified: | 13 Nov 2013 14:57 |
URI: | http://sro.sussex.ac.uk/id/eprint/31332 |
View download statistics for this item
📧 Request an update