Fixed point constructions

Self-reference is a useful technical device in logical and foundational investigations and it is often the case that self-referential constructions give rise to fixed point theorems. We survey some applications thereof, mainly concerned with: (I) type-free abstraction with contraction-free logic; (II) theories of self-applicable operations based on combinatory logic and lambda calculus. The coda illustrates the non-trivial role of pure self-referential objects with an application to the constructive foundations of mathematics. with an application to the constructive foundations of mathematics.