Directly reflective meta-programming

DOI10.1007/S10990-007-9022-0MaRDI QIDQ848742zbMATH OpenOpenAlexFDO

Authors Aaron Stump

Publication date 5 March 2010

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.489.5018

zbMATH Keywords

meta-programmingalpha equivalencechurch encodinglambda calculus, reflectionlanguage implementationMogensen-Scott encodingWand-style fexprs

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 4133469
• Meta-programming with names and necessity
• scientific article; zbMATH DE number 2018596
• Run-time manipulation of programs in a statically-typed language
• Program Logics for Homogeneous Meta-programming

Cites work

• scientific article; zbMATH DE number 2185723 (Why is no real title available?)
• scientific article; zbMATH DE number 986404 (Why is no real title available?)
• scientific article; zbMATH DE number 3821076 (Why is no real title available?)
• scientific article; zbMATH DE number 43417 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• scientific article; zbMATH DE number 1231654 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 785045 (Why is no real title available?)
• A polymorphic modal type system for Lisp-like multi-staged languages
• Combinatory logic. Vol. II
• Efficient self-interpretation in lambda calculus
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Intensional polymorphism in type-erasure semantics
• Logical frameworks
• Macros as multi-stage computations: type-safe, generative, binding macros in MacroML
• Meta Reasoning in ACL2
• Meta-programming through typeful code representation
• Meta-programming with names and necessity
• Metamathematical extensibility for theorem verifiers and proof-checkers
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Staged computation with names and necessity
• Theorem Proving in Higher Order Logics
• Towards Self-verification of HOL Light
• Typed Lambda Calculi and Applications
• Types and programing languages

Cited in

(14)

• scientific article; zbMATH DE number 2036328 (Why is no real title available?)
• Meta-programming through typeful code representation
• Sparrow: towards a new multi-paradigm language
• scientific article; zbMATH DE number 2018596 (Why is no real title available?)
• scientific article; zbMATH DE number 4133469 (Why is no real title available?)
• Incorporating quotation and evaluation into Church's type theory
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Run-time manipulation of programs in a statically-typed language
• Meta-programming through typeful code representation
• Programming in the λ-Calculus: From Church to Scott and Back
• Inter-language reflection: a conceptual model and its implementation
• Meta-programming with names and necessity
• A functional approach to generic programming using adaptive traversals
• Encoding the factorisation calculus

Describes a project that uses

Uses Software

• PoplMark
• LISP
• GHC
• Maude
• Smalltalk
• DrScheme
• Coq
• ACL2

This page was built for publication: Directly reflective meta-programming

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