Journal article
Imperative LF Meta-Programming
Electronic notes in theoretical computer science, Vol.199, pp.149-159
02/24/2008
DOI: 10.1016/j.entcs.2007.11.017
Abstract
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 meta-programming 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 soundly combining imperative features with higher-order abstract syntax. The focus of the paper is on demonstrating RSP through representative LF meta-programs.
Details
- Title: Subtitle
- Imperative LF Meta-Programming
- Creators
- Aaron Stump - Washington University in St. Louis
- Resource Type
- Journal article
- Publication Details
- Electronic notes in theoretical computer science, Vol.199, pp.149-159
- DOI
- 10.1016/j.entcs.2007.11.017
- ISSN
- 1571-0661
- eISSN
- 1571-0661
- Publisher
- Elsevier B.V
- Language
- English
- Date published
- 02/24/2008
- Academic Unit
- Computer Science
- Record Identifier
- 9984259428902771
Metrics
11 Record Views