Directly reflective meta-programming

DOI10.1007/s10990-007-9022-0zbMath1183.68164OpenAlexW2052841998MaRDI QIDQ848742

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

language implementationmeta-programmingalpha equivalencechurch encodinglambda calculus, reflectionMogensen-Scott encodingWand-style fexprs

Mathematics Subject Classification ID

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

Related Items

A functional approach to generic programming using adaptive traversals ⋮ Unnamed Item ⋮ Programming in the λ-Calculus: From Church to Scott and Back ⋮ Incorporating quotation and evaluation into Church's type theory ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics

Uses Software

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

Cites Work

• Metamathematical extensibility for theorem verifiers and proof-checkers
• Combinatory logic. Vol. II
• Meta-programming with names and necessity
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Towards Self-verification of HOL Light
• Intensional polymorphism in type-erasure semantics
• Efficient self-interpretation in lambda calculus
• Macros as multi-stage computations
• Formal certification of a compiler back-end or
• A polymorphic modal type system for lisp-like multi-staged languages
• Theorem Proving in Higher Order Logics
• Meta Reasoning in ACL2
• Typed Lambda Calculi and Applications
• Meta-programming through typeful code representation
• Staged computation with names and necessity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item