Unique Title: "Distributive-Law-Driven Synthesis of Spatial-Behavioral Type Systems from Categorical Calculus Presentations" Unique Abstract: This paper presents a constructive algorithm for synthesizing type systems and logics from formal specifications of computational calculi using 2-categorical monad theory. We show that given a 2-monad Calc representing a calculus and a 2-monad BoolAlg for Boolean algebras, a distributive law δ: Calc ∘ BoolAlg ⇒ BoolAlg ∘ Calc induces a natural interpretation of formulae as subsets of terms. The logic is generated as the free product monad Form = BoolAlg + Calc and interpreted via the composite monad BoolAlg ∘ Calc, yielding a sound and complete spatial-behavioral type system. We demonstrate that the arrow type constructor in the λ-calculus arises as a specific modal operator parametrized by application context, and we extend the framework with recursion and additional modalities to capture properties such as confinement and liveness in a reflective higher-order π-calculus. The approach is illustrated through concrete instantiations for monoids, the SKI combinator calculus, and the RHOpi calculus, establishing a uniform categorical foundation for deriving program logics and type systems from operational semantics.