The language of calculus of computable predicates as a minimal kernel for functional languages

Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement S be presented by the Hoare's triple {P(x)} S {Q(x; y)}. A total correctness of the statement S may be expressed by the formula: P(x) ⇒ [LS(S)(x; y) ⇒ Q(x; y)] & ∃y: LS(S)(x; y). Now, if one has constructed the logical semantics for a functional language, correctness of any functional program supplied with a specification can be proved. In this article, the language of Calculus of Computable Predicates (CCP) is defined as a minimal kernel for constructing the logical semantics of any pure functional language F. The CCP language includes the superposition statement, parallel statement, conditional statement, predicate and array constructor statements. The logical and operational semantics of CCP have been developed. The consistency between these semantics is proved.