What formal systems are various programming paradigms based on? I heard that functional programming paradigm is based on lambda calculus and combinatory logic. If I am correct, lambda calculus and combinatory logic are formal systems.
What  formal systems are other programming paradigms (see below) based on:


*

*logical programming paradigm (e.g. Prolog)

*procedural programming paradigm (e.g. PASCAL, C, Fortran, ALGO)

*object-oriented paradigm (e.g. SmallTalk, Eiffel, Java)?


Thanks.
 A: If I wanted to be snarky, I could say programming languages are formal systems and so they are "based on" themselves, or more pragmatically, "based on" their predecessors.  Unfortunately, this is probably the most accurate statement.  Programming paradigms are not formally or even clearly defined.  Peter Van Roy gives a much more nuanced and rigorously defined notion of "paradigm".
Functional and logic languages are often grouped together into a larger category called "declarative" languages.  In practice, these do tend to have clearer and closer ties to formal systems from logic/mathematics, though "impure" variants weaken these ties significantly.  This includes functional languages and their relationship to the lambda calculus.  This example has turned into a bit of a touchstone as the lambda calculus has proven to be dramatically more significant than originally intended.  It has applications to logic, topology, category theory, linguistics, and, of course, computer science. Limiting to just computer science, it is often used in formal semantics (particularly denotational semantics) as a basis for understanding arbitrary programming languages not just functional ones.  It's also pretty clear that "pure" functional languages such as Haskell or Agda really are little more than sugared variants of typed lambda calculi.
Logic programming languages are, of course, related to formal logic and relational algebra.  Unfortunately, Prolog has utterly dominated the mindshare of the logic programming community, and is itself far from a "pure" logic language.  It's based on a very weak fragment of first-order logic called Horn clauses and a proof search procedure for classical logic.  By moving away from classical logic, Lambda Prolog was able to expand to a much larger fragment of logic: higher-order hereditary Harrop formulas.  This allows some features, e.g. modules, to be handled in a logical way as opposed to the ad-hoc way they are handled in Prolog.  Many non-logical features of Prolog ("impurities"), such as assert/retract, were dropped in Lambda Prolog making it a much purer incarnation of logic programming.  In a different direction, Datalog is based on a weaker logic than Prolog, but also drops many of the non-logical features of Prolog and has very close connections to finite model theory.  What a formal system needs to serve as a logic programming language has been captured in the concept of an abstract logic programming language. Arguably an idealized pure Prolog might serve for logic programming a role akin to the lambda calculus for functional programming.
The contrast to declarative languages is imperative languages.  It's often stated that these are based on Turing machines, but this isn't really meaningful as very little of the theory or practice is linked back to Turing machines.  There is no generally accepted "foundational" calculus for this class of languages, unless it is the lambda calculus.  There have been, though, attempts to create such foundational calculi.  Of particular note are: Abadi's and Cardelli's $\sigma$-calculus for object oriented programming; Marc Bender's very recent Assignment Calculus for imperative programming in general; and the very pragmatic Featherweight Java for Java-like class-based OO languages.  None of these have the recognition let alone significance anywhere near the significance of the lambda calculus.
For object-oriented programming languages, there is perhaps a more compelling and fundamental basis, albeit this view is idiosyncratic.  In my opinion, many choices made in object-oriented languages can be justified by relating them to the $\pi$-calculus.  When you program in the raw $\pi$-calculus, many OO-like patterns arise.  However, a more compelling argument comes from "un-CPS transforming" the $\pi$-calculus which leads to the blue and deep blue calculi. The latter directly connects to the $\lambda$-, $\pi$-, and $\sigma$-calculi.  Of course, the $\pi$-calculus is a calculus for concurrent computation and many OO languages are not concurrent.  Historically, though, there have been a lot of ties between, particularly, message passing concurrent and object-oriented programming.
