Higher order grammar

Higher order grammar (HOG) is a grammar theory based on higher-order logic. It can be viewed simultaneously as generative-enumerative (like categorial grammar and principles and parameters) or model theoretic (like head-driven phrase structure grammar or lexical functional grammar).

Key features

There is a propositional logic of types, which denote sets of linguistic (phonological, syntactic, or semantic) entities. For example, the type NP denotes the syntactic category (or form class) of noun phrases.
HOG maintains Haskell Curry's distinction between tectogrammatical structure (abstract syntax) and phenogrammatical structure (concrete syntax).
Abstract syntactic entities are identified with structuralist (Bloomfield-Hockett) free forms (words and phrases). For example, the NP your cat is distinct from its phonology or its semantics.
Concrete syntax is identified with phonology, broadly construed to include word order.
The modelling of Fregean senses is broadly similar to Montague's, but with intensions replaced by finer-grained hyperintensions.
There is a (Curry-Howard) proof term calculus, whose terms denote linguistic (phonological, syntactic, or semantic) entities.
The term calculus is embedded in a classical higher-order logic (HOL).
The syntax-phonology and syntax-semantics interfaces are expressed as axiomatic theories in the HOL.
The HOL admits (separation-style) subtyping, e.g. NPacc, the type of accusative noun phrases, is a subtype of NP, and denotes a subset of the category denoted by NP.