This work is about using directional logic programming to give foundations to mode-correct bidirectional type systems. Reddy (1993) uses a term language for classical linear logic, adapted from Abramsky (1993)’s Linear Chemical Abstract Machine (LCHAM), to give a typed calculus for directional logic programs. We give a categorical semantics to Reddy’s calculus, using polycategories. We give normalisation results for this calculus, which shows how to evaluate logic queries to normal forms, that gives output substitutions indicating whether queries fail or succeed.