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 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