Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
I&C Journal 1995 Journal Article
Sieber has described a model of PCF consisting of continuous functions that are invariant under certain (finitary) logical relations, and shown that it is fully abstract for closed terms of up to third-order types. We show that one may achieve full abstraction at all types using a form of "Kripke logical relations" introduced by Jung and Tiuryn to characterize λ-definability.
I&C Journal 1995 Journal Article
Statman′s 1-Section Theorem (Statman, 1985a, in "Harvey Friedman′s Research on the Foundations of Mathematics" ( L. Harrington et al. , Eds.), pp. 331-338, North-Holland, Amsterdam) is an important but little-known result in the model theory of the simply typed λ-calculus. The 1-Section Theorem states a necessary and sufficient condition on models of the simply-typed λ-calculus for determining whether βη-equational reasoning is complete for proving equations that hold in a model. We review the statement of the theorem, give a detailed proof, and discuss its significance.