 On the borderline between foundational issues and applications in computer science, arguments with typical paradoxical flavor occur in the investigation of Feferman’s explicit mathematics (EM), a theory of (self-applicable) operations and non-extensional classifications. For instance, the existence of a strong power type construction leads to inconsistency in the so-called “theories of types and names”, a development of EM introduced by Jäger 1997. Paradoxical arguments are also useful for assessing the role of universes and refuting non-extensionality in EM, in presence of forms of uniform naïve comprehension (see Cantini and Minari 1999). Indeed, the role of uniformity is essential in previous investigations. Concerning naïve comprehension, it is known since the seventies (Malitz 1976) and the eighties (Weydert 1988, Forti and Hinnion 1989) that there exist nice topological models of extensionality and non-uniform naïve comprehension restricted to generalized positivity conditions. This has led to the study of so-called hyperuniverses. Additional consistency/inconsistency results about the relationship between extensionality and uniform vs. non-uniform comprehension principles can be found, e.g., in Hinnion and Libert 2003, Libert and Esser 2005. In a similar direction, recent theoretical proposals combine anew ideas from combinatory logic and lambda calculus with “inductive” reinterpretations of naïve comprehension and unrestricted truth schema, along a path already opened by Fitch in the late forties (see Scott 1975, Flagg and Myhill 1987, Aczel 1980, and Feferman 1984). Beginning with 1992, there was an attempt, due to K. Grue, to resurrect Church’s lambda calculus as a foundation of mathematics. Grue 2002 presents a very strong extension of lambda calculus, the so-called map theory, in which standard axiomatic set theory becomes interpretable, and which can be used to shed light on the difference between Russell’s and Burali-Forti’s paradoxes.