Munkám során igyekeztem a legkülönbözőbb területekről a legkorszerűbb technológiákat és kutatási eredményeket felhasználni, így szükségesnek érzem egy szakaszt szentelni a felhasznált eszközök és módszerek rövid bemutatására. A következő bekezdésekben bemutatom, hogy mit nevezünk funkcionális nyelvnek, mik ezeknek a nyelveknek a jellemző típusrendszereik, és milyen programtulajdonságokat lehet ezekkel ellenőrizni. Ezután röviden ismertetem az absztrakt interpretációt is, mint alternatívát. A fenti módszerek implementálására használt beágyazás zárja az alkalmazott módszerek ismeretetését.

A kutatás során elsősorban tisztán funkcionális nyelvek elemzésével foglalkoztam. Funkcionális nyelvek alatt azokat a programozási nyelveket nevezzük, amelyek támogatják a funkcionális programozási paradigmát. Ez egy olyan deklaratív programozási stílus, amelyben támogatják a mellékhatásmentes függvények használatát, és az olyan adatszerkezeteket, amelyek nem módosíthatóak. Az ilyen nyelvekben a függvények első rendű elemként jelennek meg, és jellemző a magasabb rendű függvények használata, valamint a fejlett típusrendszer is.

A funkcionális nyelvek között kiemelkedő helyet foglalnak el a tisztán funkcionális nyelvek. Ezek a nyelvekre teljesül a hivatkozási helyfüggetlenség. Ez azt jelenti, hogy ha egy függvényt kétszer meghívok ugyanazzal a paraméterezéssel, az eredmény ugyanaz lesz. Ezek a nyelvek egyáltalán nem támogatnak változókat és állapotokat, valamint a mellékhatásokat (fájlrendszer használat, képernyőkezelés) is közvetett módon oldják meg. Egy ilyen elterjedt megoldás a monádok használata (pl. Haskell), ahol a monádok ábrázolják a külső vagy belső állapottal végezhető műveleteket, és a programunkat ezeknek a műveleteknek a segítségével építhetjük fel anélkül, hogy a hivatkozási helyfüggetlenség sérülne.

A tisztán funkcionális nyelvek az egyszerű és tiszta elméleti alapok miatt jól tárgyalhatóak, ennek egyik bizonyítéka, hogy a típusrendszerek legnagyobb eredményei is ezekhez a nyelvekhez köthetőek. A tisztán funkcionális nyelvek a gyakran statikus típusosak, azaz ellenőrzik, hogy a függvényeket megfelelő típusú paraméterekkel hívtuk-e meg. Sőt, a legtöbb tisztán funkcionális nyelvek úgy képesek a programok típushelyességét ellenőrizni, hogy a programozónak a függvények típusait nem is kell megadnia, hanem a fordítás része a típuskikövetkeztetés (Hindley–Milner típusrendszer). Ezeknek a nyelveknek egy másik gyakori jellemzője, hogy megenged olyan típusokat, amelyek egy típusparamétertől függenek (ún. polimorf típusok). Ezt a rendszert System F-nek (vagy \(\lambda_{2}\)-nek) nevezzük.

Ha a típusrendszerben megengedjük azt is, hogy a típusaink ne csak típusparaméterektől, hanem kifejezésektől is függjenek, eljutunk a függő típusokig (\(\lambda\Pi\)). Ennek egy speciális esete a méretkódolt típusok (sized types), ahol a típusainknak nemnegatív egész paraméterei vannak, amelyek az adott típusú argumentum méretét (pl. lista esetében a hosszát) kódolják. Egy másik lehetséges bővítés az, hogy típusparaméternek nem csak típusokat, hanem tetszőleges polimorf típusokat is megengedünk (System \(F_{\omega}\), vagy \(\lambda_{\omega}\)). Ezekben a nyelvekben a típuskikövetkeztetés azonban már eldönthetetlen probléma.

A típusrendszerek fontosságára mutat rá a Curry-Howard izomorfizmus, amely azt mondja ki, hogy a függvények típusai és a függvények törzse a matematikai logika állításainak és bizonyításainak feleltethetőek meg. Ez arra használható, hogy a függvény típusába bele tudjuk kódolni a függvény bizonyos tulajdonságait is, amennyiben a típusrendszerünk elegendő kifejezőerővel bír. A fenti általánosításokra épül a Coq nyelv típusrendszere (Calculus of (Inductive) Constructions) illetve hasonló kifejezőerővel bír az Agda nyelv is, amely függő típusos (Martin-Löf–féle konstruktív típusrendszer), mely kifejezőereje megegyezik a konstruktív logikával.

A fenti példa azt mutatja, hogy tetszőleges programtulajdonság vizsgálható és bizonyítható megfelelő típusrendszerrel. A programok statikus elemzésére egy másik módszer a programok absztrakt interpretációja. Ebben a módszerben a program viselkedését közelítjük úgy, hogy tulajdonképpen egy absztrakt állapottéren futtatjuk le. Ezt a megoldás gyakran használják a fordítóprogramok a programok elemzésére (a control-flow és data-flow elemzés mellett).

Egy ilyen absztakt állapottér lehet a méretek felső korlátja. Ekkor az interpretáló függvényünk listákhoz a listák méretét rendeli. Ez a módszer nem számítja ki a listák konkrét elemeit, csak azok méreteit, ezáltal egy közelítését adja a megoldásnak.

A fejlett típusrendszerek lehetővé teszik, hogy egy gazdanyelv segítségével megfogalmazzunk egy olyan programozási nyelvet, amelyet a gazdanyelv eszközeivel írunk le és a gazdanyelv típusrendszere ellenőriz. Ennek a megoldásnak az az előnye, hogy nem kell egy programozási nyelvet újraalkotnunk, hiszen a gazda nyelv szintaktikus és szemantikus elemzőjét, de akár a kódgenerátorát is fel tudjuk használni. Másrészt a nyelvet használónak nem kell egy teljesen új nyelvet megtanulnia, hiszen a gazdanyelv eszközei a beágyazott nyelvben is rendelkezésre állhatnak (a beágyazástól függően).

A fejlett típusrendszerre azért van szükség, hogy a beágyazott nyelv típusrendszerét a gazdarendszer típusain belül kell megfogalmaznunk, amennyiben a nyelv fordítási hibáit valóban a gazdanyelv fordítási idejében akarjuk feltárni.