This topic refers to the course An introduction to type logical grammars (Catta). Here is a description and a bibliography for addressing it.
In addition to its linguistic interest, Lambek Calculus has some very interesting properties from the point of view of proof-theory. Lambek Calculus is in fact the ancestor of Linear Logic (developed by Lambek a good 30 years before the appearance of Linear Logic). We propose that students study the proof-theoretic properties of the Lambek Calculus, in particular, strong normalisation, confluence, and the fact - fundamental from a linguistic point of view - that each judgment has a finite number of proofs.
R. Moot and C. Retoré (2012), The logic of categorial grammars: a deductive account of natural language syntax and semantics, Springer, Chapter II. Available at: https://link.springer.com/chapter/10.1007/978-3-642-31555-8_2?noAccess=true
J. Lambek (1958), The mathematics of sentence structure, The American Mathematical Monthly, vol. 65, no. 3, pp. 154-170. Available at: https://www.cs.cmu.edu/~fp/courses/15816-f16/misc/Lambek58.pdf