A completeness result for the simply typed $λμ$-calculus

Simple item page
dc.creatorNour, Karim
dc.creatorSaber, Khelifa
dc.date2009-05-04
dc.date.accessioned2026-07-07T13:11:25Z
dc.date.available2026-07-07T13:11:25Z
dc.descriptionIn this paper, we define a realizability semantics for the simply typed $λμ$-calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
dc.identifierhttps://arxiv.org/abs/0905.0357
dc.identifierhttp://arxiv.org/abs/0905.0357
dc.identifierAnnals of Pure and Applied Logic (2009) 1-16
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/229278
dc.subjectLogic
dc.titleA completeness result for the simply typed $λμ$-calculus
dc.typetext

Files

Collections

arXiv