A modal analysis of staged computation
- 1 May 2001
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 48 (3) , 555-604
- https://doi.org/10.1145/382780.382785
Abstract
We show that a type system based on the intuitionistic modal logic S4 provides an expressiveframework for specifying and analyzing computation stages in the context of typed lambda-calculiand functional languages. We directly demonstrate the sense in which our calculus captures staging,and also give a conservative embedding of Nielson & Nielson's two-level functional language in ourlanguage, thus proving that binding-time correctness is equivalent to modal correctness. In addition,our...Keywords
This publication has 16 references indexed in Scilit:
- A judgmental reconstruction of modal logicMathematical Structures in Computer Science, 2001
- Programming languages capturing complexity classesACM SIGACT News, 2000
- Modal types as staging specifications for run-time code generationACM Computing Surveys, 1998
- Computational types from a logical perspectiveJournal of Functional Programming, 1998
- Monad as modalityTheoretical Computer Science, 1997
- Correctness of binding-time analysisJournal of Functional Programming, 1993
- On the unity of logicAnnals of Pure and Applied Logic, 1993
- Logic programming in the LF logical frameworkPublished by Cambridge University Press (CUP) ,1991
- A partial evaluator for the untyped lambda-calculusJournal of Functional Programming, 1991
- Semantical Analysis of Modal Logic I Normal Modal Propositional CalculiMathematical Logic Quarterly, 1963