Ariteetti- ja tietotyyppigeneerinen ohjelmointi Coq-todistusassistentilla
Authors
Date
2021Copyright
This publication is copyrighted. You may download, display and print it for Your own personal use. Commercial use is prohibited.
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 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 Coqille The 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.
Metadata
Show full item recordCollections
- Pro gradu -tutkielmat [29561]
Related items
Showing items with similar title or keywords.
-
Verkkohuijausten tyypit sosiaalisessa mediassa
Hellsten, Joonas (2017)Types of online scams in social media. In this thesis, types of online scams in social media are examined first by defining online scams and then applying the principles of them to social media setting. The thesis is a ... -
Tiedonhakijan tyypit eläiminä
Halttunen-Keyriläinen, Liisa; Korkiakangas, Ville (2012)Vastaa yhteen kysymykseen ja selvitä millainen tiedonhakija olet. Oletko koira, poro vai jokin muu? Vuoden 2012 Kirjastobasaaria varten tehty yksinkertainen peli. -
Induktiiviset tyypit
Vitikainen, Maxim (2024)Induktiiviset tyypit ovat tapa mallintaa erilaisia tietotyyppejä kuten listoja, luonnollisia lukuja ja binäärihakupuita tyyppiteoriassa. Induktiivisia tyyppejä käytetään laajasti todistusassistenteissa erilaisten teoreemojen ... -
Kriittisten järjestelmien ohjelmointi
Jolkkonen, Tomi (2019)Kriittiset järjestelmät teho-osastoilla, ydinvoimaloissa, avaruudessa ja muissa, jopa vihamielisissä ympäristöissä, suunnitellaan selviytymään yllättävistäkin tilanteista. Laitteet tai ohjelmat eivät tällaisissa paikoissa ...