UNI-MB - logo
UMNIK - logo
 
(UL)
  • A logic for algebraic effects
    Plotkin, Gordon, 1946- ; Pretnar, Matija, 1982-
    Predstavimo logiko algebrajskih učinkov, osnovano na algebrajski predstavitvi računskih učinkov z operacijami in enačbami. Začnemo z ▫$a$▫-računom, to je minimalnim računom, ki ločuje med vrednostmi, ... učinki in izračuni ter s tem kanonično določa vrstni red izvajanja. Nato ga razširimo do logike, ki je klasična večvrstna logika prvega reda s tipi višjih redov kot v Levyjevem call-by-push-value računu, načelom indukcije na izračunih, načelom proste algebre in fiksnimi točkami predikatov. Logika zaobjema Moggijev ▫$\lambda_c$▫-račun, prek definiranih modalnosti pa tudi Hennesy-Milnerjevo logiko ter evaluacijsko logiko, med tem ko je zaobjem Hoarove logike težaven.
    Vrsta gradiva - prispevek na konferenci
    Leto - 2008
    Jezik - angleški
    COBISS.SI-ID - 15624281