Gregory Meredith, Mike Stay. Logic via Distributive Laws

From Greg's message:
"We will illustrate an algorithm for generating a logic and semantics given two inputs: 1) a specification for a term language; and 2) a specification for a collection. Essentially 1 is captured as a monad, say T, and the other is captured as a monad, say C, and the logic semantics arises from a distributive law interpretation of realizability. That is, formula are interpreted as the collection of terms in T that satisfy the formula."

slides (https://drive.google.com/file/d/0BwRrcixvqFQgc255a2JiQndtZVk/view?usp=sharing)