×

zbMATH — the first resource for mathematics

Imperative LF meta-programming. (English) Zbl 1278.03067
Schürmann, C. (ed.), Proceedings of the fourth international workshop on logical frameworks and meta-languages (LFM 2004), Cork, UK, July 5, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 199, 149-159 (2008).
Summary: 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.
For the entire collection see [Zbl 1276.68030].
MSC:
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Appel, A.; Felty, A., Dependent types ensure partial correctness of theorem provers, Journal of functional programming, 14, 1, 3-19, (January 2004)
[2] Augustsson, Lennart, Cayenne – a language with dependent types, (), 239-250 · Zbl 1369.68085
[3] Barthe, G.; Cirstea, H.; Kirchner, C.; Liquori, L., Pure patterns type systems, () · Zbl 1321.68137
[4] Cormen, T.; Leiserson, C.; Rivest, R., Introduction to algorithms, (1992), MIT Press
[5] Fegaras, Leonidas; Sheard, Tim, Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space), (), 284-294
[6] N. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A Syntactic Approach to Foundational Proof Carrying-Code. In IEEE Symposium on Logic in Computer Science, 2002 · Zbl 1069.68038
[7] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, Journal of the association for computing machinery, 40, 1, 143-184, (January 1993)
[8] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Symposium on Principles of Programming Languages, pages 123-137, 1994
[9] Lena Magnusson. The Implementation of ALF—a Proof Editor Based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology and Göteborg University, 1995
[10] G. Necula and P. Lee. Proof Generation in the Touchstone Theorem Prover. In David McAllester, editor, 17th International Conference on Automated Deduction, 2000 · Zbl 0963.68523
[11] F. Pfenning. Logical Frameworks, chapter 21. Volume 2 of Robinson and Voronkov [15], 2001 · Zbl 0992.03038
[12] F. Pfenning and C. Elliott. Higher-order abstract syntax. In ACM SIGPLAN Symposium on Language Design and Implementation, 1988
[13] F. Pfenning and Carsten Schürmann. System Description: Twelf — A Meta-Logical Framework for Deductive Systems. In, 16th International Conference on Automated Deduction, 1999
[14] Pollack, Robert, Dependently typed records in type theory, Formal aspects of computing, 13, 386-402, (2002) · Zbl 1001.68013
[15] ()
[16] J. Sarnat. LF-Sigma: The Metatheory of LF with Sigma types. Technical Report 1268, Yale CS department, 2004
[17] Schürmann, C., Recursion for higher-order encodings, (), 585-599 · Zbl 0999.03039
[18] A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, July 2002 · Zbl 1010.68720
[19] A. Stump, R. Besand, J. Brodman, J. Hseu, and B. Kinnersley. From Rogue to MicroRogue. In N. Marti-Oliet, editor, International Workshop on Rewriting Logic and Applications, 2004 · Zbl 1272.68198
[20] Troelstra, A.; Schwichtenberg, H., Basic proof theory, (2000), Cambridge University Press · Zbl 0957.03053
[21] E. Westbrook, A. Stump, and I. Wehrman. A Language-based Approach to Functionally Correct Imperative Programming. In Proceedings of the 10th International Conference on Functional Programming (ICFP05), 2005 · Zbl 1302.68095
[22] D. Wu, A. Appel, and A. Stump. Foundational Proof Checkers with Small Witnesses. In D. Miller, editor, 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 264-274, 2003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.