A view of programming languages as symbiosis of meaning and computations (Q1079942)

Function and logic programming languages are understood as terms, resp. formulas, of a first order theory. This theory gives meaning to programs and allows reasoning about programs within full predicate logic possibly using quantifiers and induction. The operational semantics of programming languages is given by deductively restricted subtheories of the meaning theory in such a way that the computation sequences are in a one-to-one correspondence with proofs in subtheories. Moreover, meaning is invariant to computations as everything provable in a subtheory is required to be a theorem of the meaning theory. The questions of deadlocks and termination of programs are thus reduced to the proof-theoretical questions of existence of proofs in the subtheories.