A programozási nyelvek formális definíciói leírják azokat a statikus és dinamikus szemantikai tulajdonságokat, amelyekre fejlesztést, optimalizációt, vagy verifikációt támogató megoldásokat, nyelvspecifikus eszközöket lehet építeni. A kutatás célja a programozási nyelvek leírására használható formális nyelvek (pl. illesztési logika, típuselmélet) és alkalmazásaik vizsgálata, különös tekintettel a gépileg ellenőrizhető statikus verifikációra, és olyan megoldások keresése, amelyekkel hatásosan kapcsolhatóak össze magas szintű nyelvi leírások alacsony szintű tételbizonyítással.
előírt nyelvtudás: angol további elvárások: Jártasság a következő témákban: formális logika, formális szemantika, funkcionális programozás, formális helyességbizonyítás.