In this thesis I lift the Curry--Howard--Lambek correspondence between the simply-typed lambda calculus and cartesian closed categories to the bicategorical setting, then use the resulting type theory to prove a coherence result for cartesian closed bicategories. Cartesian closed bicategories---2-categories `up to isomorphism' equipped with similarly weak products and exponentials---arise in logic, categorical algebra, and game semantics. However, calculations in such bicategories quickly fall into a quagmire of coherence data. I show that there is at most one 2-cell between any parallel pair of 1-cells in the free cartesian closed bicategory on a set and hence---in terms of the difficulty of calculating---bring the data of cartesian closed bicategories down to the familiar level of cartesian closed categories.

In fact, I prove this result in two ways. The first argument is closely related to Power's coherence theorem for bicategories with flexible bilimits. For the second, which is the central preoccupation of this thesis, the proof strategy has two parts: the construction of a type theory, and the proof that it satisfies a form of normalisation I call local coherence. I synthesise the type theory from algebraic principles using a novel generalisation of the (multisorted) abstract clones of universal algebra, called biclones. The result brings together two extensions of the simply-typed lambda calculus: a 2-dimensional type theory in the style of Hilken, which encodes the 2-dimensional nature of a bicategory, and a version of explicit substitution, which encodes a composition operation that is only associative and unital up to isomorphism. For products and exponentials I develop the theory of cartesian and cartesian closed biclones and pursue a connection with the representable multicategories of Hermida. Unlike preceding 2-categorical type theories, in which products and exponentials are encoded by postulating a unit and counit satisfying the triangle laws, the universal properties for products and exponentials are encoded using T. Fiore's biuniversal arrows.

Because the type theory is extracted from the construction of a free biclone, its syntactic model satisfies a suitable 2-dimensional freeness universal property generalising the classical Curry--Howard--Lambek correspondence. One may therefore describe the type theory as an `internal language'. The relationship with the classical situation is made precise by a result establishing that the type theory I construct is the simply-typed lambda calculus up to isomorphism.

This relationship is exploited for the proof of local coherence. It is has been known for some time that one may use the normalisation-by-evaluation strategy to prove the simply-typed lambda calculus is strongly normalising. Using a bicategorical treatment of M. Fiore's categorical analysis of normalisation-by-evaluation, I prove a normalisation result which entails the coherence theorem for cartesian closed bicategories. In contrast to previous coherence results for bicategories, the argument does not rely on the theory of rewriting or strictify using the Yoneda embedding. I prove bicategorical generalisations of a series of well-established category-theoretic results, present a notion of glueing of bicategories, and bicategorify the folklore result providing sufficient conditions for a glueing category to be cartesian closed. Once these prerequisites have been met, the argument is remarkably similar to that in the categorical setting.