Typed self-evaluation via intensional type functions

DOI10.1145/3009837.3009853MaRDI QIDQ5370878zbMATH OpenOpenAlexFDO

Authors

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3009837.3009853

zbMATH Keywords

lambda calculusmeta-programmingself-evaluationself-interpretationself-representationtype equality

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Typed self-interpretation by pattern matching
• Breaking through the normalization barrier: a self-interpreter for F-omega
• Self-representation in Girard's System U
• Efficient self-interpretation in lambda calculus
• Metacircularity in the polymorphic \(\lambda\)-calculus

Cited in

(8)

• Metacircularity in the polymorphic \(\lambda\)-calculus
• Intensional computation with higher-order functions
• Incorporating quotation and evaluation into Church's type theory
• Self-quotation in a typed, intensional lambda-calculus
• scientific article; zbMATH DE number 177846 (Why is no real title available?)
• Typed self-interpretation by pattern matching
• Types for Proofs and Programs
• Meta-circular interpreter for a strongly typed language

This page was built for publication: Typed self-evaluation via intensional type functions

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