This research addresses problems that span several distinct but related areas of theoretical computer science: algorithms in programming languages (type inference and type checking for type systems with subtypes and recursive types, solving systems of set constraints), computational algebra (decomposition of algebraic functions, calculations of Newtonian graphs of algebraic functions), program logics and semantics (deductive systems for the propositional - calculus, typed Kleene algebra).