 One of the advantages of having different interpretations is that one sees different aspects of equality: each of these models takes a different view on what \(\lambda\)-terms get identified. The definitions of \(D_{\infty}\) and other interpretations, the verifications that they are indeed models of \(\lambda\)-calculus, and the characterizations of the \(\lambda\)-theories of these models, are beyond the scope of this entry; see (Barendregt, 1985, chapter 18) or (Meyer 1982) for details. In recent years, there is a renewed interest in the models of \(\lambda\)-calculus from the perspective of category theory and categorical logic, focusing mainly on typed \(\lambda\)-calculus (see sections  8.2  and  9.1.2  below) but also dealing with category theoretic models of the untyped \(\lambda\)-calculus discussed in this article. See, for example, (Hyland, 2017) for details.