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

Categories

Keywords

Reprint years

2009

DOI

10.1016/j.apal.2008.10.012

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,642

External links

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

Through your library

My notes

Similar books and articles

Strong normalization results by translation.René David & Karim Nour - 2010 - Annals of Pure and Applied Logic 161 (9):1171-1179.
On the semantics of the universal quantifier.Djordje Čubrić - 1997 - Annals of Pure and Applied Logic 87 (3):209-239.
On the semantics of the universal quantifier.Djordje Ubri - 1997 - Annals of Pure and Applied Logic 87 (3):209-239.
Term-Space Semantics of Typed Lambda Calculus.Ryo Kashima, Naosuke Matsuda & Takao Yuyama - 2020 - Notre Dame Journal of Formal Logic 61 (4):591-600.
Linear realizability and full completeness for typed lambda-calculi.Samson Abramsky & Marina Lenisa - 2005 - Annals of Pure and Applied Logic 134 (2-3):122-168.
Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
Third order matching is decidable.Gilles Dowek - 1994 - Annals of Pure and Applied Logic 69 (2-3):135-155.
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.
Learning based realizability for HA + EM1 and 1-Backtracking games: Soundness and completeness.Federico Aschieri - 2013 - Annals of Pure and Applied Logic 164 (6):591-617.
The Weak Normalization of the Simply Typed λse-calculus.Ariel Arbiser, Fairouz Kamareddine & Alejandro Rios - 2007 - Logic Journal of the IGPL 15 (2):121-147.

Analytics

Added to PP
2013-12-22

Downloads
17 (#213,731)

6 months
12 (#1,086,452)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Mixed logic and storage operators.Karim Nour - 2000 - Archive for Mathematical Logic 39 (4):261-280.

Add more references