swMATH ID: 29625
Software Authors: Davies, Rowan; Pfenning, Frank
Description: A modal analysis of staged computation. We show that a type system based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing computation stages in the context of typed λ-calculi and functional languages. We directly demonstrate the sense in which our λe→□-calculus captures staging, and also give a conservative embeddng of Nielson and Nielson’s two-level functional language in our functional language Mini-ML□, thus proving that binding-time correctness is equivalent to modal correctness on this fragment. In addition, Mini-ML□ can also express immediate evaluation and sharing of code across multiple stages, thus supporting run-time code generation as well as partial evaluation.
Homepage: https://dl.acm.org/citation.cfm?doid=382780.382785
Keywords: binding times; run-time code generation; staged computation
Related Software: Coq; ML; Haskell; Pesca; Links; Twelf; cubicaltt; Elf; Ynot; Agda; MetaOCaml; Nuprl; Automath; Polyp; Kleisli; Hop; Ur/Web; CDuce; Delphin; Freshml
Cited in: 49 Publications

Citations by Year