"Eesti Teadusfondi uurimistoetus" projekt ETF6940
ETF6940 "Programmiloogikad, tüübisüsteemid ja usaldusväärne koodigenereerimine (1.01.2007−31.12.2010)", Tarmo Uustalu, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
ETF6940
Programmiloogikad, tüübisüsteemid ja usaldusväärne koodigenereerimine
Program logics, type systems and trustworthy code generation
1.01.2007
31.12.2010
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ValdkondAlamvaldkondCERCS erialaFrascati Manual’i erialaProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)50,0
4. Loodusteadused ja tehnika4.4. MatemaatikaP110 Matemaatiline loogika, hulgateooria, kombinatoorika1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)50,0
PerioodSumma
01.01.2007−31.12.2007243 600,00 EEK (15 568,88 EUR)
01.01.2008−31.12.2008243 600,00 EEK (15 568,88 EUR)
01.01.2009−31.12.2009233 856,00 EEK (14 946,12 EUR)
01.01.2010−31.12.2010233 856,00 EEK (14 946,12 EUR)
61 030,00 EUR

Projekt keskendub kahele küsimusteringile programmikeelepõhistes tarkvaratehnoloogiates: imperatiivsete ja madala taseme keelte ohutuse ja korrektsuse jõustamismehhanismid ning andmevookeelte ja muude homogeensetel struktuuridel arvutamise keelte disaini ja realisatsiooni aspektid. Töötatakse välja uusi, eriti ohutusdistsipliinide jõustamisele orienteeritud programmiloogikaid ja tüübisüsteeme imperatiivsetele keeltele ning nendel baseeruvaid sertifitseerimisplatvorme. Arendatakse edasi andmevookeelte komonaadidel ja jaotusseadustel põhinevat semantika organisatsiooni, tähelepanuga andmevooprogrammide kompileerimisel automaatideks ning korrektsuse verifitseerimisel.
The project focusses on two areas of language-based software technologies: mechanisms of safety and correctness enforcement for imperative and low-level languages, and aspects of design and implementation of dataflow languages and other languages for computation on homogeneous structures. New program logics and type systems for enforcement of safety policies will be developed, together with certification platforms based thereupon. The comonad and distributive law based organization of the semantics of dataflow languages will be elaborated further, with special emphasis on compilation of dataflow programs into automata and verification of correctness.