Programming Languages and Systems

Danel Ahmani poolt pakutavad lõputööde teemad

Siin on mõned minu poolt pakutavad lõputööde teemad. Kui need teemad kohe otseselt ei kõneta, siis võib ikkagi ühendust võtta kui programmeerimiskeelte, loogika, semantika või verifitseerimise teemad huvi pakuvad.

Kontakt: Danel Ahman (danel.ahman(at)ut.ee)

Efekte sisaldavate programmide formaalne verifitseerimine keeles F*

F* [1] on tõestustele orienteeritud sõltuvalt tüübitud programmeerimiskeel, mis toetab nii efektivabade kui arvutuslikke efekte (nt mälu ja sisent-väljundi kasutamine, erindite haldamine, mitte-deterministlike ja tõenäosuslike otsuste tegemine) sisaldavate programmide verifitseerimist. Lisaks võimaldab F* tõestatud koodi kompileerimist jooksutatavaks koodiks keeltes OCaml, C või Rust.

Lõputöö selles valdkonnas sisaldaks F* keele kasutamaõppimist ning tema efektisüsteemi (Dijkstra monaadide [2] ja kihiliste efektide [3]) kasutamist mõne efekte sisaldava programmitüki või algoritmi korrektsuse spetsifitseerimiseks ja verifitseerimiseks. Lõputöö üheks eesmärgiks oleks ka demonstreerida, et F* on hea tööriist hübriidseks verifitseerimiseks, kus F* keeles implementeeritakse ja tõestatakse ainult tarkvara kriitilised komponendid, samal ajal postuleerides ülejäänud kasutatavate teekide korrektsuse.

Näiteks, üks võimalik lõputöö projekt võiks sisaldada F*'i Steel ja Pulse'i raamistike [4] kasutamist IoT seadmetes kasutatava keeles C või Rust kirjutatud sardtarkvara korrektsuse verifitseerimiseks. Parema idee saamiseks projektis tehtavast tööst võib vaadata ühte varasemat eksperimenti [5], kus natuke vanemat Low* raamistikku kasutati lihtsa katkestustepõhise ESP32 mikrokontrolleril jooksva tarkvara mälukorrektsuse tõestamiseks.

Potentsiaalsed tudengid on alati oodatud ka omi ideid välja pakkuma, et millist efekte sisaldavat tarkvaratükki või algoritmi keeles F* verifitseerida. Tudengid kes on huvitatud algoritmide verifitseerimisest teistes sõltuvalt tüübitud programmeerimiskeeltes (nt Agda, Rocq, Lean) on samuti oodatud ühendust võtma.

Peeneteralisem kommunikatsioonimudel asünkroonsetele algebralistele efektidele

Asünkroonsed algebralised efektid [1,2] on lähenemine asünkroonsete arvutuste matemaatiliselt loomulikul moel lisamiseks programmeerimiskeeltesse, mis põhinevad või kasutavad algebralisi efekte ja nende haldureid [4]. See lähenemine on modelleeritud väikeses tuum lambda-arvutuses, millel on nii tüübi- ja efektisüsteem, operatsioonisemantika kui ka prototüüpimplementatsioon [3].

Selle lõputöö eesmärgiks oleks praeguse asünkroonsete algebraliste efektide kommunikatsioonimudeli, kus sõnumid saadetakse alati kõigile osapooltele, muutmine peeneteralisemaks, et oleks võimalik programmide tüüpe kasutades staatiliselt määrata ja kontrollida, et millised paralleelsed agendid või protsessid sõnumeid kätte saavad. Selline laiendus olemasolevale teooriale ja keelele parandaks nii paralleelsete protsesside privaatsusomadusi kui ka kommunikatsiooni efektiivsust.

Sellele lõputööle võib läheneda nii teoreetilisemalt (töötades enamjaolt asünkroonsete efektide aluseks olevas lambda arvutuses) kui ka praktilisemalt (töötades enamjaolt asünkroonsete efektide prototüüpimplementatsioonis).

[1] https://doi.org/10.1145/3434305
[2] https://doi.org/10.46298/lmcs-20(3:26)2024
[3] https://github.com/matijapretnar/aeff
[4] https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf

Asünkroonsete algebraliste efektide kombineerimine efektihalduritega

Selle lõputöö eesmärgiks oleks asünkroonsetele efektidele suurema kontrolli andmine programmi jätkude (ingl continuations) üle selleks, et näiteks eemaldada mälulekked mõnedes näidetes, ning et võimaldada programmeerijatel katkestuste haldamist ise vastavalt olukorrale defineerida. Selle saavutamiseks võib kaalduda keelde lisada üldised efektihaldurid (sarnaselt sellele kuidas neid OCaml 5 keeles kasutatakse) või uurida kuidas sellist võimekust luua rohkem signaalide, katkestuste ja katkestuste haldurite põhiselt.

[1] https://doi.org/10.1145/3434305
[2] https://doi.org/10.46298/lmcs-20(3:26)2024
[3] https://github.com/matijapretnar/aeff
[4] https://homepages.inf.ed.ac.uk/slindley/papers/handlers.pdf

Haskelli DSL ajalistele ressurssidele

Ajalised ressursid [1,2] on lähenemine kuidas staatilist tüübisüsteemi kasutada selleks, et spetsifitseerida ja verifitseerida, et programmid oma käsutuses olevaid ressursse kasutaksid ajaliselt korrektselt. Näiteks koosterobotit programmeerides on vajalik, et teatud tegevused (nt mööbli kokkupanek) ei algaks liiga vara (pärast mööblitükkide värvimist). Sarnased näited on väga tavalised ka keemiliste lahuste ja protsessidega töötades või näiteks ka 3D printimises.

Ajaliste ressursside aluseks oleval lambda arvutusel on hetkel OCaml keeles implementeeritud prototüüp, mis käitub väikese eraldiseisva keelena [3,4]. Selle lõputöö eesmärgiks oleks ajalised ressursid implementeerida domeenispetsiifilise keelena (DSLina) mõnes olemasolevas keeles selleks, et ajaliste ressurssidega töötades oleks kättesaadavad ja kasutatavad ka olemasoleva keele omadused (näiteks spetsiifilised teegid ja tüübiklassid). Näiteks võib sellise DSLi luua programmeerimiskeeles Haskell (mis on sarnane FP kursuses vaadeldava keelega Idris 2) võttes inspiratsiooni teiste sarnaste programmeerimiskeelte jaoks Haskelli DSLide loomisest [5]. Samas ei ole lõputöö piiratud keelega Haskell ja kõne alla tuleks ka vastava DSLi loomine teistes keeltes (Idris 2, OCaml, ...).

Ajaliste ressursside prototüüpkeele laiendamine uute omadustega

Lõputöö eesmärgiks oleks ajaliste ressursside olemasoleva prototüüpkeele [3,4] laiendamine uute omadustega, et oleks võimalik kirja panna suuremaid, keerulisemaid ja kasulikumaid programme. Võimalike lisatavate omaduste valik on päris lai, nt ajaliste spetsifikatsioonide laiendamine ajahetkede lugemisest üldisemate sündmuste jadade kirjeldusteni, ajalisi omadusi arvesse võtva rekursiooni või iteratsiooni lisamine, polümorfismi lisamine, või keele laiendamine sobiva konkurrentsuse või paralleelsuse mudeliga.

Teine võimalik lõputöö suund oleks olemasoleva ajaliste ressursside prototüüpkeele kasutajamugavuse parendamine, nt lisades olemasolevale prototüübile süntaksi värvimise, laiendades olemasoleva veebiliidese võimalusi koodi arendamiseks, või arendades prototüüpkeelele VS Code'i plugina.

Lineaarsed ajalised ressursid

Selle lõputöö eesmärgiks oleks ajaliste ressursside kombineerimine lineaarsete või kvantitatiivsete tüüpidega. Kui ajalised ressursid kasutavad modaalseid tüüpe selleks, et kirja panna ja kontrollida millal programmid võivad oma kasutuses olevaid ressursse kasutada, siis lineaarsete või kvantitatiivsete tüüpidega tekiks võimaliks nõuda, et teatud ressursid on kasutatavad ainult täpselt ühe korra (või mingi ettemääratud arv kord), aga mitte rohkem.

Sõltuvalt sorditud algebralised teooriad konteinerandmetüüpidele

Konteinerandmetüübid [1] on matemaatiliselt loomulik ja lihtne mudel suure hulga parametriseeritud andmetüüpide (nt loendid, puud, graafid) esitamiseks läbi andmetüübi kirjelduse jagamise vastavate andmeväärtuste kujudeks ning nendes kujudes esinevateks positsioonideks (kuhu paigutatakse tegelikud andmed). Näiteks lõplike loendite kujudeks on naturaalarvud (loendite pikkused) ning kujule n vastavateks positsioonideks on naturaalarvud 0, 1, ..., n-1, ehk vastava loendi indeksid. Selliste konteinerite ja parameetriliste andmetüüpide semantika vahel on matemaatiliselt üks-ühele vastavus.

Praktikas ei ole andmetüübid aga tihti nii lihtsa struktuuriga. Näiteks loendite puhul võime rääkida sellest, et iga positsioon defineerib uue loendi, sellest positsioonist algava esialgse loendi alamloendi. Samasugused alamstruktuurid esinevad loomulikult ka puude, graafide ja teiste andmetüüpide puhul. Selliseid alamstruktuure on võimalik väga loomulikult kirjeldada ka konteinerite terminoloogias niinimetatud suunatud konteinerite abil, mis nõuavad vastavatelt konteineritelt teatud sõltuvalt tüübitud monoidi struktuuri. Samas paljud teised andmetüüpide kitsendused ei ole senini vastavaid konteineritepõhiseid omadusi omanud või on need esitused väga ebaloomuliku kujuga. Selle lõputöö eesmärgiks oleks arendada konteinerandmetüüpide jaoks sobiv sõltuvalt tüübitud algebraliste teooriate mõiste, et tekiks ühtne keel, milles kirjeldada andmetüüpide täpsemaid omadusi konteinerite tasemel. Lisaks oleks lõputöö eesmärgiks defineerida selliste algebraliste teooriate jaoks ka nende semantika ning tõestada selle korrektsus. Lõpetuseks võib huvi korral kaaluda ka vastava teegi arendamist mõnes sõltuvalt tüübitud programmeerimiskeeles (nt Agda, Rocq, Idris 2, F*).

[1] https://doi.org/10.1016/j.tcs.2005.06.002
[2] http://dx.doi.org/10.2168/lmcs-10(3:14)2014

Algebraliste efektide jooksutajate kombineerimine efektihalduritega

Algebralised efektid ja efektihaldurid [1,2] on väga aktiivne uurimisvaldkond, mille peamine kasutegur on suure hulga erinevate arvutuslike efektide (nt mälu kasutus, erindid, sisend-väljund, mittedeterminism, tõenäosus) ühetaoliselt esitamine ning nende efektide kasutajapoolse ümberdefineerimise võimaldamine. Üks silmapaistvamaid algebraliste efektide ja efektihaldurite kasutusjuhtudest on paralleelsete ja mitmelõimeliste programmide esitamine OCaml 5 keeles, võimaldades kasutajatel ise modulaarselt defineerida nende programmidele sobivaid mitmelõimelisuse mudeleid.

Samas tekitab efektihaldurite väga üldine rakendatavus tihti ka probleeme. Näiteks kui programmis töötatakse ressurssidega, mida peaks kasutama lineaarselt (st neid ei tohiks dubleerida ega niisama ära visata), nt failipointerid, siis samaaegselt üldiste efektihaldurite kasutamine võib kiiresti tekitada probleeme, kus näiteks kasutajale arusaamatult üritatakse kirjutada juba suletud faili, kuigi programmis justkui pärast faili sulgemist enam kirjutamisi ei toimu. See tuleneb sellest, et üldiste efektihalduritega on võimalik programmi erinevaid osasid mitmekordselt käivitada. Selliste probleemide jaoks on välja töötatud üldiste efektihaldurite kitsendus, efektide jooksutajad (ingl runners), mis annavad garantii, et programmid kasutavad oma ressursse lineaarselt ning kõik ressursid saavad lõpuks ka kinni pandud [3].

Selle lõputöö eesmärgiks oleks uurida, et kuidas oleks kõige parem kombineerida algebraliste efektide jooksutajaid üldiste efektihalduritega, et samaaegselt nautida nii ressursside lineaarselt kasutamise garantiisid kui ka üldiste efektihaldurite poolt pakutavat väljendusrikkust ja paindlikkust. See lõputöö võib olla nii teoreetilisem (uurides sellist kombinatsiooni algebraliste efektide aluseks olevas lambda arvutuses) kui ka praktilisem (laiendades olemasolevaid algebraliste efektide jooksutajate prototüüpe [4,5] üldiste efektihalduritega).

[1] https://doi.org/10.1007/3-540-45931-6_24
[2] https://doi.org/10.2168/LMCS-9(4:23)2013
[3] https://doi.org/10.1007/978-3-030-44914-8_2
[4] https://github.com/danelahman/haskell-coop
[5] https://github.com/andrejbauer/coop

Tehtud lõputööd

Joosep Tavits, Implementing Temporal Resources, MSc, 2025.
Ilja Sobolev, Asünkroonsete algebraliste efektidega programmeerimiskeelte normaliseerimisomadused, BSc, 2025.
Aiden Madisson, Peano aritmeetika korrektsus, BSc, 2025.
Marlene Ibrus, Konfliktivabade dubleeritud andmetüüpide formaliseerimine, BSc, 2025.
Gašper Žajdela, Operacijska semantika za jezik s časovno omejenimi viri, MSc, 2023.
Janez Radešček, Asinhroni Algebrajski Učinki, MSc, 2021.