Equality between programs with effects : doctoral dissertation
Voorneveld, Niels, 1991-
Disertacija preučuje pojem enakovrednosti programov za funkcijski programski jezik z algebrajskimi učinki in splošno rekurzijo, ki uporablja klic po naloženi vrednosti (call-by-push-value oz. na ...kratko cbpv). Osredotočamo se predvsem na vedenjsko ekvivalenco, pri čemer je obnašanje programa določeno z zbirko formul, ki so odvisne od učinkov. Dva programa istega tipa imamo za enakovredna, če zadoščata istim formulam. Za splošno interpretacijo obnašanja programa z učinki izračune ovrednotimo z drevesi, zgrajenimi iz učinkovnih operacij. Ta drevesa potem interpretiramo v logiki z modalnostmi, kar dvigne predikate na tipih vrednosti do predikatov na tipih izračunov. Eden glavnih prispevkov disertacije je določitev pogojev na modalnostih, pri katerih je vedenjska ekvivalenca, ki jo inducira logika, kongruenca. To pomeni, da enakovrednih izrazov ni mogoče razlikovati s programi. Za dokaz te lastnosti pokažemo, da vedenjska ekvivalenca sovpada z ustreznim pojmom aplikativne bipodobnosti, kjer učinke interpretiramo z uporabo relatorjev (ki dvigajo relacije). To nam omogoči, da dokažemo omenjeno kongruenco s pomočjo različice Howejeve metode. Algebrajski učinki, za katere veljajo rezultati, vključujejo napake, nedeterminizem, verjetnost, globalni pomnilnik, vhod/izhod in časomer. Z logiko lahko opišemo tudi različne kombinacije teh učinkov. Da bi lažje kombinirali učinke in naravneje opisovali obnašanje programov, posplošimo logiko na kvantitativno logiko. Tudi tu pokažemo lastnost kongruence in povezavo z aplikativno bipodobnostjo. Na koncu pokažemo, da podobni rezultati veljajo tudi, če jezik razširimo z dodatnimi konstruktorji tipov. Posebej preučimo univerzalne polimorfne in rekurzivne tipe.
Type of material - dissertation
; adult, serious
Publication and manufacture - Ljubljana : [N. Voorneveld], 2019
GS II 0000737981 glavno skladišče
GS II 737981 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
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.
Naročanje gradiva za izposojo v čitalnice
Naročanje kopij člankov
Urnik dostave gradiva z oznako DS v signaturi