izpis_h1_title_alt

Denotacijska semantika PCF
Kostelec, Kristjan (Avtor), Bauer, Andrej (Mentor) Več o mentorju... Povezava se odpre v novem oknu

.pdfPDF - Predstavitvena datoteka, prenos (564,75 KB)

Izvleček
V diplomskem delu je v celoti predstavljen funkcijski programski jezik s tipi, imenovan PCF, skupaj z njegovimi pravili za preverjanje tipov, pravili za substitucijo ter operacijsko semantiko. Dokazan je izrek o varnosti. Pokazano je, da je rekurzija negibna točka. Predstavljene so domene, ki so motivirane preko poskusa vpeljave naivne semantike. Pokazano je, da ima vsaka zvezna funkcija najmanjšo negibno točko in predstavljene so nekatere zvezne funkcije med domenami. Definirana je funkcija, ki zvezni funkciji priredi njeno najmanjšo negibno točko. Vpeljana je denotacijska semantika PCF s pomočjo domen. Dokazana sta substitucijska lema ter izrek o usklajenosti, s pomočjo logičnih relacij pa je dokazan izrek o ustreznosti. Na koncu je zapisan izrek o primernosti kot posledica izreka o usklajenosti in izreka o ustreznosti.

Jezik:Slovenski jezik
Ključne besede:programski jezik PCF, operacijska semantika, denotacijska semantika, domene, substitucijska lema, izrek o usklajenosti semantike, izrek o ustreznosti semantike, izrek o primernosti semantike
Vrsta gradiva:Diplomsko delo/naloga (mb11)
Organizacija:FMF - Fakulteta za matematiko in fiziko
Leto izida:2020
Število ogledov:75
Število prenosov:14
Metapodatki:XML RDF-CHPDL DC-XML DC-RDF
 
Skupna ocena:(0 glasov)
Vaša ocena:Ocenjevanje je dovoljeno samo prijavljenim uporabnikom.
:
Objavi na:AddThis
AddThis uporablja piškotke, za katere potrebujemo vaše privoljenje.
Uredi privoljenje...

Sekundarni jezik

Jezik:Angleški jezik
Naslov:Denotational Semantics of PCF
Izvleček:
A typed functional programming language, called PCF, is presented in this thesis together with its type checking rules, substitution rules and its operational semantics. The safety theorem is proven. It is shown that recursion is a fixed point. Domains, which are motivated by an attempt of implementing naive semantics, are presented. It is shown that every continuous function has the least fixed point and some of the continuous functions between domains are presented. A function that assigns to a continuous function its least fixed point is defined. Denotational semantics using domains is implemented. Substitution lemma and correctness theorem are proven, and soundness theorem is proved using logical relations. Computational adequacy is at the end shown as a consequence of correctness and soundness theorems.

Ključne besede:programming language PCF, operational semantics, denotational semantics, domains, substitution lemma, semantic correctness, semantic completeness, computational adequacy

Podobna dela

Podobna dela v RUL:
Podobna dela v drugih slovenskih zbirkah:

Komentarji

Dodaj komentar

Za komentiranje se morate prijaviti.

Komentarji (0)
0 - 0 / 0
 
Ni komentarjev!

Nazaj