Direct Gradually Typed Lambda Calculus with Merge Operator
Because dynamic typing and static typing have their own advantages. For example, static typing detects the error early but the dynamic typing is more flexible. It is hard to chose one of them. Fortunately, gradual typing could combine the dynamic and static typing. However, the research in gradual typing focuses on translating the source language to the casting language. We design a direct source language and prove the soundness and completeness with the blame calculus. And then add the intersection type and merge operator to the system.