A Dual-Context Sequent Calculus for S4 Modal Lambda-Term Synthesis

In type-based program synthesis, the search of inhabitants in typed calculi can be seen as a process where a specification, given by a type A, is considered to be fulfilled if we can construct a lambda-term M such that M : A, or more precisely if Gamma proves M : A holds, that is, if under some suitable assumptions Gamma the term M inhabits the type Lambda. In this paper, we tackle this inhabitation/synthesis problem for the case of modal types in the necessity fragment of the constructive logic S4. Our approach is human-driven in the sense of the usual reasoning procedures of modern theorem provers. To this purpose we employ a so-called dual-context sequent calculus, where the sequents have two contexts, originally proposed to capture the notions of global and local truths without resorting to any formal semantics. The use of dual-contexts allows us to define a sequent calculus which, in comparison to other related systems for the same modal logic, exhibits simpler typing inference rules for the square operator. In several cases, the task of searching for a term having subterms with modal types is reduced to the quest for a term containing only subterms typed by non modal propositions.