Martin Berger ; Laurence Tratt - Program Logics for Homogeneous Generative Run-Time Meta-Programming

lmcs:929 - Logical Methods in Computer Science, March 6, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:5)2015
Program Logics for Homogeneous Generative Run-Time Meta-ProgrammingArticle

Authors: Martin Berger ; Laurence Tratt ORCID

    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.


    Volume: Volume 11, Issue 1
    Published on: March 6, 2015
    Imported on: April 17, 2013
    Keywords: Computer Science - Logic in Computer Science

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1401 times.
    This article's PDF has been downloaded 522 times.