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