Berger, Martin and Tratt, Laurie (2015) Program logics for homogeneous generative run-time meta-programming. Logical Methods in Computer Science, 11 (1). ISSN 1860-5974
![]() |
PDF
- Published Version
Restricted to SRO admin only Download (466kB) |
Abstract
This paper provides the first program logic for homogeneous generative run-time meta-programming---using a variant of MiniML by Davies and Pfenning as its 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: | Article |
---|---|
Keywords: | Program Logic, Specification, Verification, Meta-Programming, Types, Observational Completeness, Descriptive Completeness, Relative Completeness, Characteristic Formula. |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Research Centres and Groups: | Foundations of Software Systems |
Depositing User: | Martin Berger |
Date Deposited: | 18 Dec 2017 15:20 |
Last Modified: | 02 Jul 2019 17:04 |
URI: | http://sro.sussex.ac.uk/id/eprint/72276 |
View download statistics for this item
📧 Request an update