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