A completeness result for the simply typed λμ-calculus

Annals of Pure and Applied Logic 161 (1):109-118 (2010)
  Copy   BIBTEX

Abstract

In this paper, we define a realizability semantics for the simply typed $lambdamu$-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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Strong storage operators and data types.Karim Nour - 1995 - Archive for Mathematical Logic 34 (1):65-78.
Some properties of the -calculus.Karim Nour & Khelifa Saber - 2012 - Journal of Applied Non-Classical Logics 22 (3):231-247.
Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
Completeness: from Gödel to Henkin.Maria Manzano & Enrique Alonso - 2014 - History and Philosophy of Logic 35 (1):1-26.
Types in logic and mathematics before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
Ordinals and ordinal functions representable in the simply typed lambda calculus.N. Danner - 1999 - Annals of Pure and Applied Logic 97 (1-3):179-201.
A General Type for Storage Operators.Karim Nour - 1995 - Mathematical Logic Quarterly 41 (4):505-514.

Analytics

Added to PP
2013-12-22

Downloads
5 (#1,344,154)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?