Show simple item record

dc.contributor.advisorKiiskinen, Sampsa
dc.contributor.advisorRossi, Tuomo
dc.contributor.authorPehkonen, Jere
dc.date.accessioned2021-04-09T06:23:21Z
dc.date.available2021-04-09T06:23:21Z
dc.date.issued2021
dc.identifier.urihttps://jyx.jyu.fi/handle/123456789/74998
dc.description.abstractTutkielman 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 uudelleenkäyttöä, mikä helpottaa lähdekoodin ylläpitoa ja vähentää yksinkertaisten virheiden määrää. Kirjasto muodostetaan Coq-todistusassistentilla, hyödyntäen sen ominaisuuksia funktionaalisena ja riippuvasti tyyppitettynä ohjelmointikielenä. Lisäksi kirjaston toteutuksessa pyritään käyttämään universumipolymorfismia toisteisten määritelmien välttämiseksi. Coqille ei ole saatavilla ariteetti- ja tietotyyppigeneeristä kirjastoa, joten kirjaston luonnin seurauksena saadaan ariteetti- ja tietotyyppigeneerisyyden tuomat edut Coqillefi
dc.description.abstractThe goal of this thesis is to create a functional library for arity-generic datatype-generic programming. Arity-generic datatype-generic programming reduces the amount of code needed and helps reuse definitions, which leads to easier maintenance and decreases the amount of simple errors. The library is done using the Coq proof assistant by using its features as a functional and dependently-typed programming language. The library will also use universe polymorphism to avoid the need for duplicated definitions in the library. There is no available arity-generic datatype-generic library for Coq so the library will bring the benefits of arity-generic datatype-generic programming to Coq.en
dc.format.extent68
dc.format.mimetypeapplication/pdf
dc.language.isofi
dc.subject.otherCoq
dc.subject.othergeneerinen ohjelmointi
dc.subject.otherpolymorfismi
dc.subject.otherriippuvat tyypit
dc.titleAriteetti- ja tietotyyppigeneerinen ohjelmointi Coq-todistusassistentilla
dc.identifier.urnURN:NBN:fi:jyu-202104092312
dc.type.ontasotPro gradu -tutkielmafi
dc.type.ontasotMaster’s thesisen
dc.contributor.tiedekuntaInformaatioteknologian tiedekuntafi
dc.contributor.tiedekuntaFaculty of Information Technologyen
dc.contributor.laitosInformaatioteknologiafi
dc.contributor.laitosInformation Technologyen
dc.contributor.yliopistoJyväskylän yliopistofi
dc.contributor.yliopistoUniversity of Jyväskyläen
dc.contributor.oppiaineTietotekniikkafi
dc.contributor.oppiaineMathematical Information Technologyen
dc.rights.copyrightJulkaisu on tekijänoikeussäännösten alainen. Teosta voi lukea ja tulostaa henkilökohtaista käyttöä varten. Käyttö kaupallisiin tarkoituksiin on kielletty.fi
dc.rights.copyrightThis publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.en
dc.type.publicationmasterThesis
dc.contributor.oppiainekoodi602
dc.subject.ysoohjelmointi
dc.format.contentfulltext
dc.type.okmG2


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record