MetaML and multi-stage programming with explicit annotations
From MaRDI portal
(Redirected from Publication:1583363)
Recommendations
Cites work
- scientific article; zbMATH DE number 3947602 (Why is no real title available?)
- scientific article; zbMATH DE number 1231578 (Why is no real title available?)
- scientific article; zbMATH DE number 236855 (Why is no real title available?)
- A modal analysis of staged computation
- A partial evaluator for the untyped lambda-calculus
- A theory of type polymorphism in programming
- DyC: An expressive annotation-directed dynamic compiler for C
- Program transformations in a denotational setting
- Two-Level Functional Languages
- Two-level semantics and abstract interpretation
- Two-level semantics and code generation
Cited in
(46)- Type and Effect System for Multi-staged Exceptions
- A type system for reflective program generators
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- Dependent Types at Work
- The \textsc{MetaCoq} project
- Static analysis of multi-staged programs via unstaging translation
- scientific article; zbMATH DE number 1670811 (Why is no real title available?)
- scientific article; zbMATH DE number 1956524 (Why is no real title available?)
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
- Automatically splitting a two-stage lambda calculus
- Incorporating quotation and evaluation into Church's type theory
- Auto in Agda. Programming proof search using reflection
- Constrained polymorphic types for a calculus with name variables
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Modality via iterated enrichment
- Classical natural deduction for S4 modal logic
- Macros as multi-stage computations: type-safe, generative, binding macros in MacroML
- scientific article; zbMATH DE number 2080286 (Why is no real title available?)
- Incremental rebinding with name polymorphism
- FabULous interoperability for ML and a linear language
- 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
- Reasoning about multi-stage programs
- Type-specialized staged programming with process separation
- Staged composition synthesis
- scientific article; zbMATH DE number 2018597 (Why is no real title available?)
- A Logical Foundation for Environment Classifiers
- A survey of strategies in rule-based program transformation systems
- Environment classifiers
- Tagless staged interpreters for typed languages
- Statically safe program generation with SafeGen
- Constructive linear-time temporal logic: proof systems and Kripke semantics
- MetaOCaml server pages: web publishing as staged computation
- A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
- The Logic of Proofs as a Foundation for Certifying Mobile Computation
- Latent Effects for Reusable Language Components
- Reasoning about multi-stage programs
- Normalization by evaluation for modal dependent type theory
- Formal Methods for Components and Objects
- scientific article; zbMATH DE number 7566057 (Why is no real title available?)
- Shifting the stage. Staging with delimited control
- Type safe incremental rebinding
- A dependently typed multi-stage calculus
- Extending the lambda-calculus with unbind and rebind
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)
