Term-space semantics of typed lambda calculus

DOI10.1215/00294527-2020-0028zbMath1486.03032OpenAlexW3116606092MaRDI QIDQ1981989

Ryo Kashima, Takao Yuyama, Naosuke Matsuda

Publication date: 7 September 2021

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1215/00294527-2020-0028

zbMATH Keywords

completenesssoundnesstyped lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Uses Software

• Automath

Cites Work

• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• A semantics for static type inference
• The completeness theorem for typing lambda-terms
• Strong normalization and typability with intersection types
• A filter lambda model and the completeness of type assignment
• Intensional interpretations of functionals of finite type I

This page was built for publication: Term-space semantics of typed lambda calculus