Self-quotation in a typed, intensional lambda-calculus

DOI10.1016/J.ENTCS.2018.03.024OpenAlexW2803077385WikidataQ113317556 ScholiaQ113317556MaRDI QIDQ2130593

C. Barry Jay

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.024

zbMATH Keywords

type theorycombinatorslambda-calculusself-interpretation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Coq
• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Conflicting accounts of \(\lambda\)-definability
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Programs as data structures in \(\lambda\)SF-calculus
• The self-reduction in lambda calculus
• \(\lambda\)-definability and recursiveness
• Self-Representation in Girard's System U
• Breaking through the normalization barrier: a self-interpreter for f-omega
• Tagless staged interpreters for typed languages
• A combinatory account of internal structure
• A modal analysis of staged computation
• First-class patterns
• Pattern Calculus
• Efficient self-interpretation in lambda calculus
• Introduction to generalized type systems
• Typed self-interpretation by pattern matching
• Typed self-evaluation via intensional type functions
• Linear-time self-interpretation of the pure lambda calculus
• Primitive recursion for higher-order abstract syntax

This page was built for publication: Self-quotation in a typed, intensional lambda-calculus