Efficient self-interpretation in lambda calculus

DOI10.1017/S0956796800000423zbMath0817.68051MaRDI QIDQ4764616

Torben Ægidius Mogensen

Publication date: 6 August 1995

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

lambda calculus

Mathematics Subject Classification ID

Logic programming (68N17) Combinatory logic and lambda calculus (03B40)

Related Items

Self-quotation in a typed, intensional lambda-calculus ⋮ Gödelization in the lambda calculus ⋮ Unnamed Item ⋮ Unified Syntax with Iso-types ⋮ From realizability to induction via dependent intersection ⋮ Directly reflective meta-programming ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Many more predecessors: A representation workout ⋮ Unnamed Item ⋮ The calculus of dependent lambda eliminations ⋮ The \textsc{MetaCoq} project ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ A lean specification for gadts: System F with first-class equality proofs ⋮ The Impact of the Lambda Calculus in Logic and Computer Science ⋮ The self-reduction in lambda calculus ⋮ Programs as data structures in \(\lambda\)SF-calculus ⋮ Programming in the λ-Calculus: From Church to Scott and Back ⋮ ASMs and Operational Algorithmic Completeness of Lambda Calculus ⋮ Unnamed Item ⋮ The development of a partial evaluator for extended lambda calculus ⋮ Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages ⋮ An investigation of Jones optimality and BTI-universal specializers ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Unnamed Item

Uses Software

• Scheme

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Typed representation of objects by functions
• A partial evaluator for the untyped lambda-calculus