VSE knjižnice (vzajemna bibliografsko-kataložna baza podatkov COBIB.SI)
13.
Effective metatheory for type theory : PhD thesis
Haselwarter, Philipp Georg
V disertaciji definiram končne teorije tipov kot širok razred teorij tipov v stilu Martina-Löfa in oblikujem programski jezik za izpeljevanje sodb v splošnih teorijah tipov. Sodobne računalniške ...implementacije teorije tipov se zanašajo na njeno računsko interpretacijo bodisi preko rezultatov o odločljivosti ali realizabilnosti. Takšni rezultati pa niso na voljo za vse teorije tipov, ki jih srečamo v literaturi, zato njihova implementacija predstavlja izziv. Radi bi implementirali fleksibilen dokazovalni pomočnik, ki omogoča, da uporabnik sam določi teorijo tipov. Za to pa potrebujemo splošno definicijo teorije tipov, ki oriše njeno strukturo. V disertaciji podam matematično natančno definicijo razreda končnih teorij tipov, ki pokrije znane primere, vključno z ekstenzionalno teorijo tipov, računom konstrukcij in homotopsko teorijo tipov. Najprej se osredotočim na matematični razvoj končnih teorij tipov, preden se posvetim njihovi implementaciji v dokazovalnih pomočnikih. Definicija je zgrajena po stopnjah. Začnemo s surovo sintakso, surovimi pravili in surovimi teorijami tipov, nato razmejimo končna pravila in teorije tipov ter na koncu opredelimo standardne teorije tipov. S temi definicijami lahko dokažemo tudi metateoretične rezultate kot sta izrek o enoličnosti tipov in izrek o eliminaciji rezov. Da bi končne teorije tipov lažje implementirali v dokazovalnem pomočniku, jih preoblikujem v kontekstno neodvisne teorije tipov, ki omogočajo pravilno ravnanje s prostimi spremenljivkami. Definicija kontekstno neodvisnih teorij tipov je ponovno zgrajena po stopnjah. Za vsako stopnjo dokažem primerne metaizreke. Formalizma končnih torij tipov in kontekstno neodvisnih teorij tipov sta povezana preko izrekov prevedbe. Uvedem metajezik Andromeda (AML), učinkovni programski jezik, ki omogoča priročno ravnanje s sodbami in pravili v kontekstno neodvisnih teorijah tipov, ki jih uporabnik lahko sam določi. Jezik tudi podpira običajne tehnike za razvoj dokazov. AML izkoristi algebrajske učinke in poganjalce, da na modularen način z lokalnimi hipotezami razširi algoritme v dokazovalnih pomočnikih. Operacijska semantika jezika AML se naslanja na dvosmerno tipiziranje in pomaga uporabniku unovčiti informacije o kontekstu. S tem pokaže uspešno interakcijo z operacijami učinkov. AML je implementiran v dokazovalnem pomočniku Andromeda. Opišem tudi prve poskuse razvoja kontekstno neodvisnih teorij tipov z računalniško pomočjo v AML.
Vrsta gradiva - disertacija
; neleposlovje za odrasle
Založništvo in izdelava - Ljubljana : [P. G. Haselwarter], 2021
Bibliografsko gradivo je bilo uspešno dodano na polico.
Dodajanje bibliografskega gradiva na polico ni uspelo.
Gradivo je že na polici.
Trajna povezava
URL:
Faktor vpliva
Dostop do baze podatkov JCR je dovoljen samo uporabnikom iz Slovenije. Vaš trenutni IP-naslov ni na seznamu dovoljenih za dostop, zato je potrebna avtentikacija z ustreznim računom AAI.
Leto
Faktor vpliva
Izdaja
Kategorija
Razvrstitev
JCR
SNIP
JCR
SNIP
JCR
SNIP
JCR
SNIP
Izberite knjižnično izkaznico:
Baze podatkov,
v katerih je revija indeksirana
Ime baze podatkov
Področje
Leto
Povezave do osebnih bibliografij avtorjev
Povezave do podatkov o raziskovalcih v sistemu SICRIS
Storitev za pridobivanje naslova trenutno ni dostopna, prosimo, poskusite še enkrat.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in naslov za dostavo ter dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrani naslov za dostavo in dokončali postopek rezervacije.
Obvestilo
Trenutno je storitev za avtomatsko prijavo in rezervacijo nedostopna. Gradivo lahko rezervirate sami na portalu Biblos ali ponovno poskusite tukaj kasneje.
Citiranje
Funkcionalnost trenutno ni na voljo. Prosimo, poskusite kasneje.
