memo is a new domain-specific probabilistic programming language meant for reasoning about reasoning. In this extended abstract, we present a formalization of memo, including a type system and a denotational semantics.