A theory of mixin modules: algebraic laws and reduction semantics