Operacijska semantika za jezik s časovno omejenimi viriŽajdela, Gašper (Avtor) Pretnar, Matija (Mentor) Ahman, Danel (Komentor) lambda računčasovno omejeni virimodalni tipiizrek o varnostiteorija enačbskladnostformalizacijaLambda račun je eden izmed osnovnih matematičnih modelov računanja, kjer uporabljamo le spremenljivke, funkcije (abstrakcije) in aplikacije funkcij. Lahko ga razširimo s tipi in tako dobimo tipizirani lambda račun, ki je jedro funkcijskih programskih jezikov. Tipi v jeziku zagotavljajo varnost, saj preprečujejo, da bi programer na primer seštel število in niz. V delu predstavimo problem, ki nastane pri uporabi jezika v industriji, kjer mora med določenimi procesi preteči dovolj časa. Želimo si, da to reši že sistem tipov. Obstoječi sistemi, kot je OCamlov, tega ne omogočajo. Sistem tipov razširimo z modalnim tipom, ki zagotovi, da vira ne uporabimo, če ni prej preteklo dovolj časa. Za pravilno delo s tovrstnim tipom poskrbita operaciji odvijanje in zavijanje. V tem delu za tovrstni jezik podamo operacijsko semantiko, kjer si za pravilno delo s časovno omejenimi viri pomagamo s stanjem. Dokažemo izrek o varnosti, torej da bo vsak program napisan v tem jeziku ohranil tip in da bo v vsakem trenutku naredil korak, ali pa se ustavil. V delu definiramo enačbe za teorijo enačb za delo s časovno omejenimi viri in dokažemo, da je operacijska semantika skladna s teorijo enačb. Vsi rezultati, razen nekaterih primerov v dokazu skladnosti, so formalizirani z dokazovalnim pomočnikom Agda.20232023-09-14 08:15:19Magistrsko delo/naloga150138sl