Quantifiers in lambda calculus
There is no notion of quantification in the standard $\lambda$-calculus as introduced by Church. As far as I can tell from Liang's paper, it deals with a specialized version of $\lambda$-calculus in which $\lambda$-expressions can be logical expressions containing quantifiers and logical connectives. This approach is meant as a way of formally representing natural language statements. Thus, we are really dealing with an applied $\lambda$-calculus with function symbols that correspond to logical connectives and function symbols and are to be interpreted in this way.