Incremental Bidirectional Type Checking

• Built algorithm to make bidirectional type checking incremental.
• Use case: structural editor.
• Key problem: scope management.
• Might introduce/delete bindings during AST editing, and thus introduce/delete shadowing.
• Solution: Each node have an order maintenance interval, tree inclusion relationship get translated to interval inclusion relationship.
• Data structure to manage intervals, so a heavy-light decomposition on AST is possible.
• Formalize the whole type system via Marked and Annotated Lambda Calculus (MALC) and prove correctness in Agda.
• Result: huge speedup against from scratch computation.