A Curry-Howard Approach to Church's Synthesis via Linear Logic

Church synthesis problem asks whether or not one can synthesize a 1-Lipschitz (or synchronous) function according to a specification of the type ∀ X ∃ Y φ(X,Y) expressed in the language of MSO over ω.

A (costly) algorithm has been exhibited in the work Büchi-Landweber and Rabin, which is able to determine whether such a synchronous function exists, and if it does, returns a finite-state transducer realizing the specification.  

We propose a theory LMSO based on linear logic, together with its semantics. LMSO embeds MSO in the sense that there exists a translation of MSO formulas φ ⟼ φ^L such that MSO ⊢ φ iff LMSO ⊢ φ^L. It refines MSO(ω) by allowing to interpret Church's synthesis problem in the sense that LMSO ⊢ ∀ X ∃ Y φ^L(X,Y) if and only if there exists a finite-state transducer M such that MSO ⊢ ∀ X φ(X,M(X)).

If time allows, I will sketch how LMSO may be completely axiomatized. The proof of completeness uses in a crucial way a translation of formulas extremely similar to Gödel's Dialectica interpretation for arithmetic.