We introduce syntax and semantics of a basic programming language.

We define derivation rules for a higher-order strictness typing system.

We proof soundness of our system with respect to the semantics.

The proof is formalized by using a theorem prover.

In inference algorithm is specified which infers principal strictness types.

An extension of our system with recursive data types is given.