HKU PL Group

We are a group of programming language researchers who study topics about functional language design, type theory, compilers and program analysis.
The University of Hong Kong

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.