  Church's synthesis problem asks whether there exists a finite-state stream
transducer satisfying a given input-output specification. For specifications
written in Monadic Second-Order Logic (MSO) over infinite words, Church's
synthesis can theoretically be solved algorithmically using automata and games.
We revisit Church's synthesis via the Curry-Howard correspondence by
introducing SMSO, an intuitionistic variant of MSO over infinite words, which
is shown to be sound and complete w.r.t. synthesis thanks to an automata-based
realizability model.
