Reference of the connection of category theory and logic(foundation of mathematics)

The connections between category theory and logic are manifold and deep. However, they usually don't directly revolve around foundations. Most(All?) attempts at categorical foundations didn't really go anywhere which is not to say they didn't produce anything. Most interest in categorical foundations has been on topos theoretic foundations. Lambek's work on the free topos is one example. To be clear, most categorist, like most mathematicians, have no special interest in foundations, even categorists focusing on topos theory which arose from algebraic geometry. The nLab page on foundations of mathematics gives some idea of the feeling categorists have toward foundations.

I'll return to foundations in a bit, but I'll shift away toward applications of category theory. Jacobs' book Categorical Logic and Type Theory discusses the machinery needed to connect categories to logic. Modular correspondence between dependent type theories and categories including pretopoi and topoi serves as a handy reference for how explicitly the internal language and internal logic work in various important examples. This nLab page gives a quick high-level view. A key part of this is these description are fairly "modular" meaning to a large extent we can mix-and-match logical features as desired. Sheaves in Geometry and Logic is a good book introducing topos theory and how it connects to (surprise!) geometry and logic. It assumes you have the basics of category theory down, e.g. as you would get from Awodey's book.

Shifting back towards foundations, while category theory suggests some conceptual/philosophical viewpoints like the principle of equivalence which may present usual presentations, at least, of set theory in a negative light, in my opinion, one of the most valuable ways category theory is useful for thinking about foundations is the plethora of models it provides. Want to explore what the world of math looks like if it is finitist or predicative or predicative-finitist? Then I have a pretopos for you. Or better, the internal language of a suitable class of pretoposes. Going a different direction, Paul Cohen introduced the technique of forcing in his proof of the independence of the Continuum Hypothesis. Categorically, forcing corresponds to constructing categories of sheaves which can serve as models of ZFC. This is described in chapter VI of Sheaves in Geometry and Logic. The many models of classical set theory that can be produced this way caused Cohen to change his philosophical stance on mathematics.

Most of these models are presented as models within a background powerful set theory, e.g. Tarksi-Grothendieck set theory, though this set theory is usually not articulated but rather it is just assumed that there is enough set theory to perform the categorical constructions. These models usually can be formulated as first-order theories like ZFC set theory or, alternatively, deductive systems for the internal languages can directly formulated, but usually the categorists are just studying types of categories and are not trying to put forward a foundational system.

The main reference for category theory is:

• S. Mac Lane. Categories for the Working Mathematician (2nd edition). Springer, 1998.

Other general references for category theory are:

• S. Awodey. Category Theory. Oxford University Press, 2010.
• S. Abramsky, N. Tzevelekos. Introduction to Categories and Categorical Logic. Lecture Notes in Physics, Vol. 813, pages 3-94, Springer, 2011.

More specific and advanced references for your question (see in particular the last item, which is within a current mainstream research) are:

• F.W. Lawvere. The Category of Categories as a Foundation for Mathematics. Proceedings of the Conference on Categorical Algebra, Springer-Verlag, 1–21, 1966.

• R. Goldblatt. Topoi: The Categorical Analysis of Logic. Elsevier, 1979.

• J.L. Bell. Categories, Toposes and Sets. Synthese, 51 (3): 293–337, 1982.

• J.L. Bell. Toposes and Local Set Theories: An Introduction. Oxford University Press, 1988.

• J. Couture, J. Lambek. Philosophical Reflections on the Foundations of Mathematics. Erkenntnis, 34 (2): 187–209, 1991.

• S. Awodey et al. (The Univalent Foundations Program), Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.

Let me add a couple of different suggestions. If you want a more discursive overview of how category theory relates to some traditional issues in the foundations of mathematics, the following might well be of interest:

• Ralf Krömer, Tool and Object: A History and Philosophy of Category Theory (Birkaüser, 2007)

• Jean-Pierre Marquis, From a Geometrical Point of View: Study of the History and Philosophy of Category Theory (Springer, 2009).

Other categorical resources (this time freely available online, and including four handbook essays on categorical logic if your interest goes in that direction) are mentioned on this Category Theory webpage.