magistrsko delo
Žiga Zupančič (Avtor), Matija Pretnar (Mentor)

Povzetek

V delu je predstavljen funkcijski programski jezik Eff za delo z algebrajskimi učinki in njihovimi prestrezniki. Na primeru je prikazan prevod v OCaml in predstavljena učinkovitost izvajanja glede na ročno napisano kodo v OCaml-u. Opisana je optimizacija prevajanja in kakšne težave pri tem nastanejo. Kot rešitev je predstavljen eksplicitno tipiziran jezik ExEff z eksplicitnimi učinki in ciljni jezik tega jezika. Kot drug možen ciljni jezik je predstavljen eksplicitno tipiziran jezik NoEff, ki ne vsebuje eksplicitnih učinkov, sledi le njihovi uporabi. Dokazana sta izreka o ohranitvi ter delnem napredku za NoEff s spremljajočimi lemami. Opisana so pravila za prevajanje tipov, pretvorb, vrednosti in izračunov iz ExEff v NoEff. Podan je primer prevoda in dokazan je izrek o ohranitvi tipov. Na kratko je razložena tudi implementacija v jeziku OCaml, kjer predstavimo strukturo in nekatere dele kode.

Ključne besede

računski učinki;prestrezniki algebrajskih učinkov;eksplicitni tipi;jezik brez eksplicitnih učinkov;

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.09 - Magistrsko delo
Organizacija: UL FMF - Fakulteta za matematiko in fiziko
Založnik: [Ž. Zupančič]
UDK: 004.4
COBISS: 25937155 Povezava se bo odprla v novem oknu
Št. ogledov: 1614
Št. prenosov: 207
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: Elaboration of algebraic effect handlers to a language without effects
Sekundarni povzetek: In this work a functional programming language based on algebraic effect handlers, called Eff, is presented. It is shown on an example how it is translated to OCaml and how efficient its execution is in comparison to hand-written OCaml code. A compilation optimization is described and so are the difficulties of it. As a solution an explicitly typed language with explicit dirt, called ExEff, is presented and a backend for it. As another possible backend an explicitly typed language, called NoEff, is presented, which does not include explicit dirt but it tracks its use. Preservation and partial progress theorems are proved for NoEff with the corresponding lemmas. Rules for elaborating types, coercions, values and computations from ExEff to NoEff are described. An example of elaboration is given and the type preservation theorem is proved. Implementation to OCaml is briefly explained containing structure information and parts of the code.
Sekundarne ključne besede: computational effects;algebraic effect handlers;explicit types;language without explicit effects;
Vrsta dela (COBISS): Magistrsko delo/naloga
Študijski program: 0
Konec prepovedi (OpenAIRE): 1970-01-01
Komentar na gradivo: Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Računalništvo in matematika - 2. stopnja
Strani: IX, 59 str.
ID: 11555481