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.

References in zbMATH (referenced in 45 articles )

Showing results 1 to 20 of 45.
Sorted by year (citations)

1 2 3 next

  1. Birkedal, Lars; Clouston, Ranald; Mannaa, Bassel; Ejlers Møgelberg, Rasmus; Pitts, Andrew M.; Spitters, Bas: Modal dependent type theory and dependent right adjoints (2020)
  2. del Carmen González Huesca, Lourdes; Miranda-Perea, Favio E.; Linares-Arévalo, P. Selene: Axiomatic and dual systems for constructive necessity, a formally verified equivalence (2019)
  3. Jay, Barry: Intensional computation with higher-order functions (2019)
  4. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  5. Costa Seco, João; Ferreira, Paulo; Lourenço, Hugo: Capability-based localization of distributed and heterogeneous queries (2017)
  6. Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
  7. Francez, Nissim: On harmony and permuting conversions (2017)
  8. Jacinto, Bruno; Read, Stephen: General-elimination stability (2017)
  9. Kavvos, G. A.: On the semantics of intensionality (2017)
  10. Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans Bugge; Birkedal, Lars: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types (2016)
  11. de Paiva, Valeria; Ritter, Eike: Fibrational modal type theory (2016)
  12. Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)
  13. Więckowski, Bartosz: Subatomic natural deduction for a naturalistic first-order language with non-primitive identity (2016)
  14. Berger, Martin; Tratt, Laurence: Program logics for homogeneous generative run-time meta-programming (2015)
  15. Read, Stephen: General-elimination harmony and higher-level rules (2015)
  16. Beklemishev, Lev; Gurevich, Yuri: Propositional primal logic with disjunction (2014)
  17. Bonelli, Eduardo; Steren, Gabriela: Hypothetical logic of proofs (2014)
  18. Francez, Nissim: Harmony in multiple-conclusion natural-deduction (2014)
  19. Francez, Nissim: A logic inspired by natural language: quantifiers as subnectors (2014)
  20. Francez, Nissim: Bilateralism in proof-theoretic semantics (2014)

1 2 3 next