Efficient self-interpretation in lambda calculus

DOI10.1017/S0956796800000423MaRDI QIDQ4764616zbMATH OpenFDO

Authors 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)

Recommendations

• Linear-time self-interpretation of the pure lambda calculus
• scientific article; zbMATH DE number 1522992
• The self-reduction in lambda calculus

Cites work

• scientific article; zbMATH DE number 5654346 (Why is no real title available?)
• A partial evaluator for the untyped lambda-calculus
• Metacircularity in the polymorphic \(\lambda\)-calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Typed representation of objects by functions

Cited in

(32)

• Call-by-value lambda calculus as a model of computation in Coq
• scientific article; zbMATH DE number 515729 (Why is no real title available?)
• The \textsc{MetaCoq} project
• Programs as data structures in \(\lambda\)SF-calculus
• The Impact of the Lambda Calculus in Logic and Computer Science
• ASMs and operational algorithmic completeness of lambda calculus
• Directly reflective meta-programming
• The development of a partial evaluator for extended lambda calculus
• An investigation of Jones optimality and BTI-universal specializers
• Binary lambda calculus and combinatory logic
• The self-reduction in lambda calculus
• Self-quotation in a typed, intensional lambda-calculus
• From realizability to induction via dependent intersection
• scientific article; zbMATH DE number 2084341 (Why is no real title available?)
• Unified syntax with iso-types
• The calculus of dependent lambda eliminations
• Degrees of extensionality in the theory of Böhm trees and Sallé's conjecture
• Gödelization in the lambda calculus
• scientific article; zbMATH DE number 7226008 (Why is no real title available?)
• Many more predecessors: a representation workout
• Programming in the λ-Calculus: From Church to Scott and Back
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• A lean specification for gadts: System F with first-class equality proofs
• Typed self-interpretation by pattern matching
• Typed self-evaluation via intensional type functions
• scientific article; zbMATH DE number 1522992 (Why is no real title available?)
• Linear-time self-interpretation of the pure lambda calculus
• Encoding the factorisation calculus
• ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
• Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
• Weak call-by-value lambda calculus as a model of computation in Coq
• scientific article; zbMATH DE number 7204439 (Why is no real title available?)

Describes a project that uses

Uses Software

• Scheme

This page was built for publication: Efficient self-interpretation in lambda calculus

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