Imperative LF Meta-Programming

12 years 5 months ago
Imperative LF Meta-Programming
Logical frameworks have enjoyed wide adoption as meta-languages for describing deductive systems. While the techniques for representing object languages in logical frameworks are relatively well understood, languages and techniques for metaprogramming with them are much less so. This paper presents work in progress on a programming language called Rogue-Sigma-Pi (RSP), in which general programs can be written for soundly manipulating objects represented in the Edinburgh Logical Framework (LF). The manipulation is sound in the sense that, in the absence of runtime errors, any putative LF object produced by a well-typed RSP program is guaranteed to type check in LF. An important contribution is an approach for combining imperative features with higher-order abstract syntax. The focus of the paper is on demonstrating RSP through representative LF meta-programs. Key words: Meta-Programming, Logical Frameworks, Rewriting Calculus
Aaron Stump
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Aaron Stump
Comments (0)