Program logics for homogeneous generative run-time meta-programming

DOI10.2168/LMCS-11(1:5)2015MaRDI QIDQ5177336zbMATH OpenFDO

Authors Martin Berger, Laurence Tratt

Publication date 11 March 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1411.4256

zbMATH Keywords

verificationtypesspecificationprogram logicrelative completenessmeta-programmingcharacteristic formulaobservational completenessdescriptive completeness

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

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.

Recommendations

• Program Logics for Homogeneous Meta-programming
• Meta-programming with names and necessity
• Equivalent transformations of heterogeneous meta-programs
• Imperative LF meta-programming
• Formal Methods for Components and Objects

Cited in

(7)

• Mumbo: a rule-based implementation of a run-time program generation language
• Equivalent transformations of heterogeneous meta-programs
• A program logic for fresh name generation
• Program Logics for Homogeneous Meta-programming
• Reasoning about multi-stage programs
• Formal Methods for Components and Objects
• A dependently typed multi-stage calculus

Describes a project that uses

Uses Software

• MiniML

This page was built for publication: Program logics for homogeneous generative run-time meta-programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5177336)