In order to make programs sound and correct in semantics, people have proposed type systems [1]} to ensure such significant properties. A well-typed programming language is determined by two semantic properties: preservation and progress. The first property makes sure that types are invariant under the evaluation and typing rules. And the progress property says a well-typed program never gets stuck. Nevertheless, little attention has been put on equipping formal languages good at dynamic modeling and reasoning, like situation calculus, with strong typing mechanisms. Indeed, situation Calculus is a typed second-order formal language, but from the viewpoint of type checking, it is not enough to finish smoothly. For instance, in situation calculus, only typed quantifiers are introduced for basic variables, while as for other logical expressions consisting of variables and connectives, fluents and predicates, current situation calculus emphasizes little on how to type check whether they are well-typed, how to type them thoroughly. Therefore, equipping other elements in current version of situation calculus with types is greatly needed for a complete and robust programming language with its type system, which is definitely feasible according to our investigation.
