"Higher Order Grammar" 

Carl Pollard

The key idea is to treat syntactic types as types not of the Lambek 
calculus but rather of a more mainstream type theory along the lines 
of Church 1940, Henkin 1950, Gallin 1975, and (the boolean bivalent 
version of) Lambek and Scott 1986. On this approach a grammar is a 
theory in a classical higher-order logic (CHOL) and linguistic expressions 
are denoted by higher-order terms. The type system for such a grammar 
is a full intutitionistic propositional logic (IPL); and the categorical 
models are bivalent boolean toposes. Among those, the set-theoretic 
models (i.e. the well-pointed toposes, which are essentially Henkin 
models augmented with product types and (separation) subtypes) are of 
special interest because their familiarity to linguists (via Ty2) makes 
working with HOG very easy and intuitive: for example, a context-free 
grammar rule is just a function whose domain is a product of syntactic 
types and whose codomain is a syntactic type. And a linguistic expression 
is a just a member of (the set which interprets) its type, but by the
Curry-Howard isomorphism (the standard one, not a resource-sensitive
analog) it also corresponds to a proof of its own type (more
precisely, an equivalence class of such proofs).

Like HPSG, this architecture enables one to think of linguistic
entities model-theoretically and view the nonlogical axioms of the
grammar as constraints; but like TLG, it enables one to think of
syntactic categories as propositions in an intuitionistic logic and of
linguistic expressions as being associated with proofs. But the
constraint logic (a form of classical HOL) is more familiar and easy
to work with than the special-purpose logic (RSRL) employed in HPSG,
and the type logic (IPL) is more familiar (to everyone but
type-logical grammarians) than the Lambek calculus. Thus it bridges
the mathematical and sociological gap between the constraint-based and
type-logical grammar communities while being (in terms of formal
prerequisites) more familar and accessible than either HPSG or
standard TLG. An added bonus is that phonological and semantic
entities can be treated together with the syntactic ones in the same
theory (and the same model), with phonological and semantic
interpretation being type-indexed families of functions
(categorically, they are (partial) logical endofunctors).

Although the nature of HOG is clarified for specialists by thinking of
it in categorical terms, the existence of the set theoretic models
makes it accessible to anyone familiar with a set-theory/logic
background at the level of (say) the Dowty, Wall, and Peters
text. This is the level at which the course would be taught, primarily
through presentation of an illustrative English fragment,