The Meaning of Types From Intrinsic to Extrinsic Semantics

A definition of a typed language is said to be "intrinsic" if it assigns<br />meanings to typings rather than arbitrary phrases, so that ill-typed<br />phrases are meaningless. In contrast, a definition is said to be "extrinsic"<br />if all phrases have meanings that are independent of their typings,<br />while typings represent properties of these meanings.<br />For a simply typed lambda calculus, extended with recursion, subtypes,<br />and named products, we give an intrinsic denotational semantics<br />and a denotational semantics of the underlying untyped language. We<br />then establish a logical relations theorem between these two semantics,<br />and show that the logical relations can be "bracketed" by retractions<br />between the domains of the two semantics. From these results, we<br />derive an extrinsic semantics that uses partial equivalence relations.

Higher-order intersection types and multiple inheritance

We study a natural generalization of SystemFωwith intersection types, establishing basic structural properties and constructing a semantic model based on partial equivalence relations to prove the soundness of typing. As an application of this calculus, we define a simple typed model of object-oriented programming with multiple inheritance.

Least fixpoints of endofunctors of cartesian closed categories

Least fixpoints are constructed for finite coproducts of definable endofunctors of Cartesian closed categories that have weak polynomial products and joint equalizers of arbitrary families of pairs of parallel arrows. Both conditions hold in PER, the category whose objects are partial equivalence relations on N, and whose arrows are partial recursive functions. Weak polynomial products exist in any cartesian closed category with a finite number of objects as well as in any model of second order polymorphic lambda calculus: that is, in the proof theory of any second order positive intuitionistic propositional calculus, but such a category need not have equalizers. However, any finite coproduct of definable endofunctors of a cartesian closed category with weak polynomial products will have a least fixpoint in a larger category with equalizers whose objects are right ideals (or sieves) of modulo certain congruence relations, and whose arrows are induced from .

Layered Predicates

We review the concept of logical relations and how they interact with structural induction, furthermore we give examples of their use, and of particular interest is the combination with the PER-idea (partial equivalence relations). This is then generalized to Kripke logical relations; the major application is to show that in combination with the PER-idea this solves the problem of establishing a substitution property in a manner oonducive to structural induction. Finally we introduce the concept of Kripke-layered predicates; this allows a modular definition of predicates and supports a methodology of ''proofs in stages'' where each stage forcuses on only one aspect and thus is more manageable. All of these techniques have been tested and refined in ''realistic applications'' that have been documented elsewhere.

Building domains from graph models

In this paper we study partial equivalence relations (PERs) over graph models of the λcalculus. We define categories of PERs that behave like predomains, and like domains. These categories are small and complete; so we can solve domain equations and construct polymorphic types inside them. Upper, lower and convex powerdomain constructions are also available, as well as interpretations of subtyping and bounded quantification. Rather than performing explicit calculations with PERs, we work inside the appropriate realizability topos: this is a model of constructive set theory in which PERs, can be regarded simply as special kinds of sets. In this framework, most of the definitions and proofs become quite smple and attractives. They illustrative some general technicques in ‘synthetic domain theory’ that rely heavily on category theory; using these methods, we can obtain quite powerful results about classes of PERs, even when we know very little about their internal structure.