Akademska digitalna zbirka SLovenije - logo
VSE knjižnice (vzajemna bibliografsko-kataložna baza podatkov COBIB.SI)
  • Applications of algebraic effect theories : doctoral thesis
    Lukšič, Žiga
    Algebrajski učinki so uveljavljena metoda za modeliranje računskih učinkov v funkcijskem programiranju. Učinke predstavimo z operacijami, pomen pa jim dodelimo s prestrezniki. Teorije algebrajskih ... učinkov so sestavljene iz signature, ki poda tipe operacij, in enačb, ki opisujejo njihovo obnašanje. Vsi prestrezniki morajo biti skladni s predpisano teorijo; prestreznik ne sme razlikovati med programi, ki jih v dani teoriji smatramo za enake. Teorije učinkov so običajno globalne, torej morajo vsi prestrezniki spoštovati isto množico enačb, kar omeji nabor možnih prestreznikov. Mnogo kasnejših pristopov zato enačbe odmisli, kar sicer olajša uporabo prestreznikov, vendar močno omeji možnosti dokazovanja lastnosti programov ob prisotnosti računskih učinkov, kjer enačbe igrajo ključno vlogo. V doktorskem delu predstavimo jezik ▫$EEFF$▫, ki z uporabo lokalnih teorij učinkov omili omejitve enotne teorije učinkov, saj omogoči uporabo različnih teorij v različnih delih programa. Za varnost poskrbi sistem tipov, nadgrajen z zmožnostjo sledenja teorijam učinkov, ki omogoča varno uporabo prestreznikov. Sistemu tipov je pridružena logika, v kateri preverjamo pravilnost prestreznikov. Za logiko imamo na voljo več možnosti, kar nam omogoča izbiro najprimernejše logike glede na problem. Zdravost logike določimo z uporabo denotacijske semantike, ki temelji na delnih ekvivalenčnih relacijah. Jezik ▫$EEFF$▫ je formaliziran v dokazovalnem pomočniku Coq in implementiran kot razširitev programskega jezika Eff. Formalizacija hkrati služi kot orodje za dokazovanje ekvivalence programov in vsebuje dve različni logiki, za kateri pokažemo zdravost. V doktorskem delu podamo več primerov, ki predstavijo prednosti uporabe lokalnih teorij algebrajskih učinkov.
    Vrsta gradiva - disertacija ; neleposlovje za odrasle
    Založništvo in izdelava - Ljubljana : [Ž. Lukšič], 2020
    Jezik - angleški
    COBISS.SI-ID - 43657475

    Povezava(-e):

    Repozitorij Univerze v Ljubljani – RUL

Knjižnica/institucija Kraj Akronim Za izposojo Druga zaloga
FMF in IMFM, Matematična knjižnica, Ljubljana Ljubljana MAKLJ v čitalnico 1 izv.
Narodna in univerzitetna knjižnica, Ljubljana Ljubljana NUK v čitalnico 1 izv.
ni za izposojo 1 izv.
loading ...
loading ...
loading ...

Vnos na polico