In this talk, I will try to convince you that type checking can be seen as logic programs with a fine-grained input-output system, and query evaluations are proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, via direct translation from bidirectional typing rules to a logic programming language. The current work in progress is to extend the logic programming language with more constructs to accommodate more expressive type systems.
This is based on joint work with Vikraman Choudhury and Neel Krishnaswami.
