One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.

In this paper we investigate two purely syntactical notions ofcircularity, which we call ``self-application'''' and ``self-inclusion.'''' Alanguage containing self-application allows linguistic items to beapplied to themselves. In a language allowing for self-inclusion thereare expressions which include themselves as a proper part. We introduceaxiomatic systems of syntax which include identity criteria andexistence axioms for such expressions. The consistency of these axiomsystems will be shown by providing a variety of different models –these models being our circular languages. Finally we will show what (...) apossible semantics for these circular languages could look like. (shrink)