Induktiiviset tyypit
Tekijät
Päivämäärä
2024Tekijänoikeudet
Julkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.
Induktiiviset tyypit ovat tapa mallintaa erilaisia tietotyyppejä kuten listoja, luonnollisia lukuja ja binäärihakupuita tyyppiteoriassa. Induktiivisia tyyppejä käytetään laajasti todistusassistenteissa erilaisten teoreemojen ja tietokoneohjelmien toteutukseen. Yleistys induktiivisista tyypeistä ovat korkeammat induktiiviset tyypit, jotka laajentavat induktiivisia tyyppejä mahdollistamalla tyypin alkioiden välisten ekvivalenssirelaatioiden määrittämisen. Tässä kirjallisuuskatsauksessa käsitellään induktiivisten ja korkeampien induktiivisten tyyppien teoriaa, niiden toteutuksia eri
ohjelmointikielissä sekä erilaisia sovelluskohteita. Inductive types are a way to represent complex datatypes such as lists, natural numbers and binary search trees in type theory. Inductive types are currently widely used in proof assistants to implement mathematical theorems and computer
programs. A generalization of inductive types are higher inductive types, which extend inductive types by making it possible to define equivalence relations between inhabitants of a type. This thesis explores theory behind inductive and higher inductive types, their implementations in different programming languages and their use cases.
Asiasanat
Metadata
Näytä kaikki kuvailutiedotKokoelmat
- Kandidaatintutkielmat [5319]
Samankaltainen aineisto
Näytetään aineistoja, joilla on samankaltainen nimeke tai asiasanat.
-
Ariteetti- ja tietotyyppigeneerinen ohjelmointi Coq-todistusassistentilla
Pehkonen, Jere (2021)Tutkielman tavoitteena on luoda toimiva kirjasto ariteetti- ja tietotyyppigeneeristä ohjelmointia varten. Ariteetti- ja tietotyyppigeneerinen ohjelmointi edesauttaa toisteisen lähdekoodin määrän vähentämistä sekä määritelmien ... -
Metatieto tietovarastoympäristössä
Niemijärvi, Ville (2002)
Ellei toisin mainittu, julkisesti saatavilla olevia JYX-metatietoja (poislukien tiivistelmät) saa vapaasti uudelleenkäyttää CC0-lisenssillä.