MetaML and multi-stage programming with explicit annotations

DOI10.1016/S0304-3975(00)00053-0zbMath0949.68047OpenAlexW2094455839MaRDI QIDQ1583363

T. Sheard, Walid Taha

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

zbMATH Keywords

calculusFunctional programmingprogramming language semanticshigh-level program generationmulti-level languagesmulti-stage languagestype-safetytype-systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (26)

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 ⋮ Latent Effects for Reusable Language Components ⋮ 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

• Unnamed Item
• MiniML

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