Can lambda-calculus be used for knowledge representation?

Question

Natural language semantics (in computational linguistics) uses lambda terms for expressing the semantics of natural language sentences. There is vast literature about combinatorial categorial grammars and lambda semantics of natural language, e.g. tutorial about framework http://yoavartzi.com/tutorial/

The question is - if lambda calculus can be used to represent the meaning of the natural language text, then can we use lambda calculus for the universal representation of knowledge? Why there are so few results in this direction? Or maybe there are efforts to bridge the meaning as expressed in lambda calculus with some of the common knowledge representation approaches?

Maybe (extended) Curry-Howard isomorphism between lambda calculus and logical/deductive systems can be used to translate the semantics in terms of lambda calculus into knowledge in terms of logical expressions, e.g., maybe translation to description logics and action logics is possible?