Type Checking is Proof Reductions in Classical Linear Logic
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…
