Abstract:The full combination of if-expression and subtyping was known as a challenging problem for a long time. The difficulty comes from the fact that two branches of an if-expression might have different types and these types might not have a unique least upper bound. Such situation could happen in real object oriented languages such as Java. In our previous work, we investigated this problem in a simply typed lambda calculus extended with subtyping and if-expression and solved the type checking problem in that system. In this paper, we extend the result to bounded quantification combined with if-expression.