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