A modal analysis of staged computation
作者： Rowan Davies , Frank Pfenning
关键词:
摘要: We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in context of functional languages. Our main technical result is conservative embedding Nielson & Nielson's two-level language our Mini-ML, thus proving binding-time correctness equivalent to this fragment. In addition Mini-ML can also express immediate evaluation sharing code across multiple stages, supporting run-time generation as well partial evaluation.
core.ac.uk
sci-hub.se 参考文章(35)
Mark Leone, Peter Lee, Lightweight Run-Time Code Generation. partial evaluation and semantic-based program manipulation. pp. 97- 106 ,(1994)
Frank Pfenning, Logic programming in the LF logical framework Logical Frameworks. pp. 149- 182 ,(1991) , 10.1017/CBO9780511569807.008
Neal Nelson, Tim Sheard, Type safe abstractions using program generators ,(1995)
Neil D. Jones, Efficient Algebraic Operations on Programs algebraic methodology and software technology. pp. 393- 420 ,(1991)
John Hatcliff, Mechanically Verifying the Correctness of an Offline Partial Evaluator international symposium on programming language implementation and logic programming. pp. 279- 298 ,(1995) , 10.1007/BFB0026826
Mark Leone, Peter Lee, Deferred Compilation: The Automation of Run-Time Code Generation Deferred Compilation: The Automation of Run-Time Code Generation. ,(1993) , 10.21236/ADA274124
Peter Sestoft, Neil D. Jones, Carsten K. Gomard, Partial evaluation and automatic program generation ,(1993)
Martin Hofmann, A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursion Computer Science Logic. pp. 275- 294 ,(1998) , 10.1007/BFB0028020
Simone Martini, Andrea Masini, A Computational Interpretation of Modal Proofs Springer Netherlands. ,vol. 2, pp. 213- 241 ,(1996) , 10.1007/978-94-017-2798-3_12
Brian F. Chellas, Modal Logic: An Introduction ,(1980)