MetaML and multi-stage programming with explicit annotations

DOI10.1016/S0304-3975(00)00053-0zbMATH Open0949.68047OpenAlexW2094455839MaRDI QIDQ1583363FDOQ1583363

Walid Taha, Tim Sheard

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

Recommendations

• A metalogic programming approach: language, semantics and applications
• Tools and Algorithms for the Construction and Analysis of Systems
• A generalized approach to metaprogramming in logic grammars
• scientific article; zbMATH DE number 1208121
• scientific article; zbMATH DE number 1956524

zbMATH Keywords

programming language semanticscalculusFunctional programminghigh-level program generationmulti-level languagesmulti-stage languagestype-safetytype-systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• A theory of type polymorphism in programming
• DyC: An expressive annotation-directed dynamic compiler for C
• A modal analysis of staged computation
• Title not available (Why is that?)
• Program transformations in a denotational setting
• Two-Level Functional Languages
• Two-level semantics and abstract interpretation
• Two-level semantics and code generation
• A partial evaluator for the untyped lambda-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (37)

• Type and Effect System for Multi-staged Exceptions
• Dependent Types at Work
• A type system for reflective program generators
• Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
• The \textsc{MetaCoq} project
• Title not available (Why is that?)
• Title not available (Why is that?)
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
• Incorporating quotation and evaluation into Church's type theory
• Modality via iterated enrichment
• Classical natural deduction for S4 modal logic
• Title not available (Why is that?)
• Incremental rebinding with name polymorphism
• Automatically Splitting a Two-Stage Lambda Calculus
• MetaKlaim: a type safe multi-stage language for global computing
• Implicitly heterogeneous multi-stage programming
• Experiences with an object-oriented, multi-stage language
• Gaussian elimination: a case study in efficient genericity with MetaOCaml
• Type-specialized staged programming with process separation
• A Logical Foundation for Environment Classifiers
• Auto in Agda
• Title not available (Why is that?)
• A survey of strategies in rule-based program transformation systems
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Statically safe program generation with SafeGen
• MetaOCaml server pages: web publishing as staged computation
• A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
• Latent Effects for Reusable Language Components
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Normalization by evaluation for modal dependent type theory
• Formal Methods for Components and Objects
• Title not available (Why is that?)
• Type safe incremental rebinding
• A dependently typed multi-stage calculus
• Title not available (Why is that?)
• Extending the lambda-calculus with unbind and rebind

Uses Software

• ML
• MiniML

This page was built for publication: MetaML and multi-stage programming with explicit annotations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1583363)