Projekt keskendub programmeerimisteooria jaoks huvipakkuvate intuitsionistlike ja seonduvate loogikate teooriale ning rakendustele. Uuritakse püsipunktioperaatoritega ja sisukat kategoorset interpretatsiooni omavate modaalsustega intuitsionistlike süsteemide, duaalse intuitsionistliku loogika ning mitmesuguste intermediaarloogikate tõestussüsteeme, kategoorset semantikat ja termiarvutusi. Niisuguste loogikate termiarvutused on käsitletavad induktiivseid, koinduktiivseid tüüpe, abstraktseid arvutustüüpe ja juhtimisoperaatoreid toetavate baasfunktsionaalkeeltena. Eesmärgiks on saada uusi teoreetilisi tulemusi vaadeldavate loogikasüsteemide kohta ning arendada rakendusi programmikeeltes ja programmeerimismetoodikas. Projekt jätkab ETFi projekti 4155 (2000-02).
The project focusses on the theory and applications of intuitionistic and related logics with relevance for programming theory. Specifically, proof systems, categorical semantics and term calculi are studied for intuitionistic systems with fixedpoint operators and with modalities admitting a respectable categorical interpretation, dual intuitionistic logic, and various intermediate logics. Term calculi for these systems are basic functional languages featuring inductive, coinductive types, abstract computation types, and control operators. The goal is to obtain new theoretical results about the logics and to develop new applications in programming languages and programming methodology. The project is a continuation to ETF project 4155 (2000-02).