UP - logo
(UL)
  • The logic and handling of algebraic effects
    Pretnar, Matija, 1982-
    Disertacija obravnava logiko in prestreznike algebrajskih učinkov. Ti so računski učinki, ki jih lahko predstavimo z algebrajskimi teorijami, na primer izjeme, nedeterminizem, interaktivni vhod in ... izhod, pomnilnik, ter njihove kombinacije. V prvem delu predlagamo logiko algebrajskih učinkov. Začnemo z vpeljavo ▫$a$▫-računa, ki je minimalna logika z enačbami, katere namen je izpostavitev specifičnih lastnosti algebrajskih učinkov. V nadaljevanju predstavimo vsestransko logiko, ki gradi na rezultatih, dobljenih v ▫$a$▫-računu. Tipi in izrazi logike so enaki tistim iz Levyjevega pristopa call-by-push-value, pravila sklepanja pa so standardna pravila klasične večvrstne logike prvega reda s predikati, razširjena s fiksnimi točkami predikatov ter algebrajskima načeloma, ki opisujeta univerzalnost prostih modelov teorije za dane učinke. Logiko nato uporabimo za sklepanje o lastnostih programov z učinki ter za prevod Moggijevega ▫$\lambda_c$▫-računa, Hennesy-Milnerjeve logike in Moggijeve različice Pittsove evaluacijske logike. V drugem delu uvedemo prestreznike algebrajskih učinkov. Ti prestreznike izjem ne le predstavijo v algebrajskem pristopu, temveč jih posplošijo na poljubne algebrajske učinke. Takšni prestrezniki ustrezajo modelom teorije, ki predstavlja učinke, stavke za njihovo uporabo pa interpretiramo s homomorfizmi, porojenimi z univerzalno lastnostjo prostega modela. Prestreznike uporabimo za opis mnogih poprej nepovezanih konceptov iz teorije in prakse, na primer preimenovanja in skrivanja v CSS-ju, preusmeritve tokov, prekinitve čakanja ter popravkov stanja po sproženih izjemah.
    Vrsta gradiva - disertacija ; neleposlovje za odrasle
    Založništvo in izdelava - Edinburgh : [M. Pretnar], 2010
    Jezik - angleški
    COBISS.SI-ID - 15623769

Knjižnica Signatura – lokacija, inventarna št. ... Status izvoda
FMF in IMFM, Matematična knjižnica, Ljubljana Skladišče-Jadranska 19

10965/29
prosto - za čitalnico
loading ...
loading ...
loading ...