Efficient self-interpretation in lambda calculus

DOI10.1017/S0956796800000423zbMATH Open0817.68051MaRDI QIDQ4764616FDOQ4764616

Authors: Torben Ægidius Mogensen 

Publication date: 6 August 1995

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

Recommendations

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

zbMATH Keywords

lambda calculus

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A partial evaluator for the untyped lambda-calculus
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Typed representation of objects by functions

Cited In (32)

• Call-by-value lambda calculus as a model of computation in Coq
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• 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
• Many more predecessors: a representation workout
• Programming in the λ-Calculus: From Church to Scott and Back
• Gödelization in the lambda calculus
• Title not available (Why is that?)
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Typed self-interpretation by pattern matching
• A lean specification for gadts: System F with first-class equality proofs
• Typed self-evaluation via intensional type functions
• Title not available (Why is that?)
• Linear-time self-interpretation of the pure lambda calculus
• Encoding the factorisation calculus
• ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
• Weak call-by-value lambda calculus as a model of computation in Coq
• Title not available (Why is that?)
• Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation

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)