​​​Denis Firsov​

Projekt uurib uusi sõltuvate tüüpidega tüübisüsteme, mis on sobilikud programmeerimiskeelte semantikate arendamiseks ja formaliseerimiseks tõestusassistentide abil. Eriline rõhk on keeltel, mis toetavad konkurentsust ja mittedetermiminismi, nt oleku-siirdesüsteemid ja protsessiarvutused. Populaarsed tüübiteoreetilised tõestusassistendid nagu Agda ja Coq ei sobi niisuguste keelte denotatsioonsemantika esitamiseks, kuna nende tüübisüsteemid ei ole piisavalt väljendusvõimsad. Me vastame sellele väljakutsele sel moel, et toome kaasaegsetesse tüübiteoreetilistesse raamistutesse nagu homotoopiline tüübiteooria sisse uue klassi koinduktiivseid tüüpe, mis esitavad saavutatavate funktorite terminaalseid koalgebraid. Denotatsioonsemantikas läheb protsesside mittedeteministliku ja interageeruva käitumise esitamiseks vaja tüüpe just sellest klassist. Loodavad väljendusvõimsamad tüübisüsteemid lubavad konkurentsuse ja mittedeterminismiga keelte formaalset semantikat adekvaatselt kodeerida.

"Eesti IT Tippkeskus EXCITE ühendab kõiki Eesti edukaid IT teadusgruppe ühtseks, sünergiat loovaks teaduskeskuseks, vähendades niimoodi Eesti teadusmaastiku killustatust ning luues sünergiat erinevate teadusteemade vahel. Konsortsium arendab edasi matemaatiliste mudelite verifitseerimise ning andmeanalüüsi teooriaid, millele toetudes töötatakse omakorda välja meetodid veakindlate ning turvaliste IT süsteemide ehitamiseks. Neid meetodeid rakendatakse küberfüüsiliste süsteemide, robotite, e-tervise teenuste ning biomeditsiiniteenuste näitel. EXCITE koosneb kümnest, täpse ülesandepüstitusega ning kindla metoodikaga alamteemast, mille fookust projekti eluea jooksul vastavalt vahetulemustele kohendatakse. EXCITE suurendab Eesti teaduse jätkusuutlikust, luues 20-30 doktorandile ning järeldoktorile toetava keskkonna ning pideva rahastuse.

The central research focus of the technology and economics of trust in software theme will be certified software. Topics of research include: • methods and tools for certification of software; program analysis, transformation, generation; in particular for big data, cloud and IoT; • static analysis (model checkers, theorem provers), verification, systematic testing; • contract languages, languages with powerful type systems (refinement types, dependent types); domain-specific languages; • program synthesis and program learning, program understanding; • repositories of certified software, evolution of certified software; • trust in closed-source software, gradual trust-building; • trading trust, pricing of trust, game theory of trust.