MetaML and multi-stage programming with explicit annotations
From MaRDI portal
Publication:1583363
DOI10.1016/S0304-3975(00)00053-0zbMath0949.68047OpenAlexW2094455839MaRDI QIDQ1583363
Publication date: 26 October 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00053-0
calculusFunctional programmingprogramming language semanticshigh-level program generationmulti-level languagesmulti-stage languagestype-safetytype-systems
Related Items (25)
Modality via iterated enrichment ⋮ Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages ⋮ Auto in Agda ⋮ Type-specialized staged programming with process separation ⋮ Normalization by evaluation for modal dependent type theory ⋮ Type safe incremental rebinding ⋮ The \textsc{MetaCoq} project ⋮ A survey of strategies in rule-based program transformation systems ⋮ Extending the lambda-calculus with unbind and rebind ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Implicitly heterogeneous multi-stage programming ⋮ Classical natural deduction for S4 modal logic ⋮ Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code ⋮ Statically safe program generation with SafeGen ⋮ A type system for reflective program generators ⋮ Dependent Types at Work ⋮ Unnamed Item ⋮ The Logic of Proofs as a Foundation for Certifying Mobile Computation ⋮ Automatically Splitting a Two-Stage Lambda Calculus ⋮ Incremental rebinding with name polymorphism ⋮ Unnamed Item ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ⋮ A Logical Foundation for Environment Classifiers ⋮ A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4 ⋮ Constructive linear-time temporal logic: proof systems and Kripke semantics
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Two-level semantics and abstract interpretation
- Two-level semantics and code generation
- A theory of type polymorphism in programming
- DyC: An expressive annotation-directed dynamic compiler for C
- A modal analysis of staged computation
- Program transformations in a denotational setting
- Two-Level Functional Languages
- A partial evaluator for the untyped lambda-calculus
This page was built for publication: MetaML and multi-stage programming with explicit annotations