| Journal: | Computación y sistemas |
| Database: | |
| System number: | 000560694 |
| ISSN: | 1405-5546 |
| Authors: | Miranda Perea, Favio E.1 Omaña Silva, Sammantha2 González Huesca, Lourdes del Carmen1 |
| Institutions: | 1Universidad Nacional Autónoma de México, Facultad de Ciencias, México 2Universidad Nacional Autónoma de México, Instituto de Investigaciones en Matemáticas Aplicadas y en Sistemas, México |
| Year: | 2022 |
| Season: | Abr-Jun |
| Volumen: | 26 |
| Number: | 2 |
| Pages: | 787-799 |
| Country: | México |
| Language: | Inglés |
| English abstract | 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 λ-term M such that M : A, or more precisely if Γ ⊢ M : A holds, that is, if under some suitable assumptions Γ the term M inhabits the type A. In this paper, we tackle this inhabitation/synthesis problem for the case of modal types in the necessity fragment of the constructive logic S 4. 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 □ 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. |
| Keyword: | Dual-context sequent calculus, Constructive necessity, Type inhabitation, Modal lambda calculus, Program synthesis |
| Full text: | Texto completo (Ver HTML) Texto completo (Ver PDF) |
