A revised completeness result for the simply typed -calculus using realizability semantics

DOI10.23638/LMCS-13(3:13)2017MaRDI QIDQ5367052zbMATH OpenOpenAlexFDO

Authors Mohamad Ziadeh, Karim Nour

Publication date 12 October 2017

Full work available at URL https://arxiv.org/abs/1612.09223

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Abstract: In this paper, we define a new realizability semantics for the simply typed lambda-mu-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. We also prove a completeness result of our realizability semantics using a particular term model. This paper corrects some errors in [21] by the first author and Saber.

Recommendations

• A completeness result for the simply typed \(\lambda \mu \)-calculus
• The \(\lambda \mu^{\mathbf{T}}\)-calculus
• Sound and complete typing for \(\lambda\mu\)
• scientific article; zbMATH DE number 1222571
• Term-space semantics of typed lambda calculus

Cited in

(6)

• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• scientific article; zbMATH DE number 2185676 (Why is no real title available?)
• On completeness and parametricity in the realizability semantics of System \textsf{F}
• Normalization in the simply typed -calculus
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
• A completeness result for the simply typed \(\lambda \mu \)-calculus

This page was built for publication: A revised completeness result for the simply typed \(\lambda\mu\)-calculus using realizability semantics

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