The proposed language of $Σ$-expressions provides a formal method for proving properties of algorithms. The idea of this approach is based on the concept of $Σ$-formulae of first order predicate calculus defining recursively enumerable sets over a constructive model. The language of $Σ$-expressions of the author is typed, i.e. every expression has its type. Every normal term is a $Σ$-expression of type 0. Every Boolean combination of elementary formulae $P(t\sb 1,...,t\sb n)$ is a $Σ$-expression of type B (the type of formulae). If $Φ$ is an expression of type $(τ\sb 1,...,τ\sb n\vert τ)$ and $Φ\sb 1,...,Φ\sb n$ are expressions of types $τ\sb 1,...,τ\sb n$, then the composition $Φ(Φ\sb 1,...,Φ\sb n)$ is an expression of type $τ$. Similarly, the expressions of the form ($\exists xΦ)$, ($\forall x\in yΦ)$, ($\exists x\in yΦ)$, $Φ$, [R;$Φ$ ] are introduced. They give, intuitively, constructive operations over constructive models, like for instance $Φ$ giving the least fixed point of $Φ$ (R). In the paper the formal system of calculi for $Σ$-expressions is presented. Some examples showing that normal programming operators like composition, branching, recursion etc. are expressible in the language stress the connection with programming theory. There is no problem also with embedding logic programming into $Σ$-expressions. The paper ends with simple examples of formal proofs.
Reviewer: A.Kreczmar