| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4662225 | Annals of Pure and Applied Logic | 2009 | 10 Pages |
Abstract
In 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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
