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