University of Sussex
Browse

File(s) under permanent embargo

Program logics for homogeneous meta-programming

chapter
posted on 2023-06-08, 10:04 authored by Martin BergerMartin Berger, Laurence Tratt
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.

History

Publication status

  • Published

Publisher

Springer Verlag

Volume

6355 L

Page range

64-81

Pages

18.0

Event name

16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)

Event location

Dakar, Senegal

Event type

conference

Book title

Logic for Programming, Artificial Intelligence, and Reasoning

ISBN

3642175104

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Notes

Proceedings 16th International Conference, LPAR-16, Dakar, Senegal, April 25--May 1, 2010

Full text available

  • No

Peer reviewed?

  • Yes

Editors

A Voronkov, E M Clarke

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC