Ariteetti- ja tietotyyppigeneerinen ohjelmointi Coq-todistusassistentilla

Abstract

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.