Hindman's theorem, ultrafilters, and reverse mathematics

Assuming CH. Hindman [2] showed that the existence of certain ultrafilters on the power set of the natural numbers is equivalent to Hindman's Theorem. Adapting this work to a countable setting formalized in RCA 0 , this article proves the equivalence of the existence of certain ultrafilters on countable Boolean algebras and an iterated form of Hindman's Theorem, which is closely related to Milliken's Theorem. A computable restriction of Hindman's Theorem follows as a corollary.