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.
Type of material - dissertation
; adult, serious
Publication and manufacture - Ljubljana : [Ž. Lukšič], 2020
GS II 0000740925 glavno skladišče
GS II 740925 glavno skladišče
available - reading room
Shelf entry
Adding material to shelf was successful.
Adding material to shelf failed.
It was not necessary to add the material to the shelf.
Bibliographic material was successfully added on shelf.
Adding bibliographical material on shelf was not successful.
Material is already on the shelf.
Permalink
URL:
Impact factor
Access to the JCR database is permitted only to users from Slovenia. Your current IP address is not on the list of IP addresses with access permission, and authentication with the relevant AAI accout is required.
Year
Impact factor
Edition
Category
Classification
JCR
SNIP
JCR
SNIP
JCR
SNIP
JCR
SNIP
Impact factor
Select the library membership card:
DRS,
in which the journal is indexed
Database name
Field
Year
Links to authors' personal bibliographies
Links to information on researchers in the SICRIS system
Subject headings in COBISS General List of Subject Headings
Select pickup location
The material from the parent unit is free. If the material is delivered to the pickup location from another unit, the library may charge you for this service.
