-
Effective metatheory for type theory : PhD thesisHaselwarter, Philipp GeorgV 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 odrasleZaložništvo in izdelava - Ljubljana : [P. G. Haselwarter], 2021Jezik - angleškiCOBISS.SI-ID - 94707203
Povezava(-e):
Repozitorij Univerze v Ljubljani – RUL
Digitalna knjižnica Slovenije - dLib.siDostop z namenskih računalnikov v prostorih NUK
Avtor
Haselwarter, Philipp Georg
Drugi avtorji
Bauer, Andrej
Teme
Matematična logika |
Disertacije |
matematika |
odvisna teorija tipov |
algebrajska teorija |
dokazovalni pomočnik |
metajezik |
računski učinki |
mathematics |
dependent type theory |
algebraic theory |
proof assistant |
metalanguage |
computational effects
![loading ... loading ...](themes/default/img/ajax-loading.gif)
Knjižnica/institucija |
Kraj | Akronim | Za izposojo | Druga zaloga |
---|---|---|---|---|
FMF in IMFM, Matematična knjižnica, Ljubljana | Ljubljana | MAKLJ |
v čitalnico 1 izv.
|
|
Narodna in univerzitetna knjižnica, Ljubljana | Ljubljana | NUK |
v čitalnico 1 izv.
|
ni za izposojo 1 izv.
|
![loading ... loading ...](themes/default/img/ajax-loading.gif)
![loading ... loading ...](themes/default/img/ajax-loading.gif)
![loading ... loading ...](themes/default/img/ajax-loading.gif)
Vnos na polico
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 |
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 |
---|---|
Haselwarter, Philipp Georg | 39334 |
Bauer, Andrej | 15854 |
Izberite prevzemno mesto:
Prevzem gradiva po pošti
Obvestilo
Gesla v Splošnem geslovniku COBISS
Izbira mesta prevzema
Mesto prevzema | Status gradiva | Rezervacija |
---|
Prosimo, počakajte trenutek.