A Core Erlang az Erlang programozási nyelv egy rész- és köztes nyelve, így rendelkezik az Erlang jellegzetes tulajdonságaival, mint például a részleges függvényalkalmazások hiánya, mohó kiértékelés, dinamikus típusellenőrzés, és az aszinkron kommunikáció konkurensen futó folyamatok között. Ebben a kutatásban a Core Erlang szekvenciális résznyelvét vizsgáljuk különböző definíciós stílusokban (small- és big-step szemantikákkal), illetve a konkurens Core Erlang szemantikáját definiáljuk egy small-step megközelítéssel. A téma kiterjed a definíciók kiértékelésére, összehasonlítására, a különböző szemantikák alkalmazásaira is (mint például programok helyességének bizonyítása). Az alkalmazások közül kiemelendő a programok ekvivalenciájának vizsgálata, amelyre alapozva vizsgáljuk programtranszformációk (pl. refaktorálások, optimalizációk) helyességét. A kutatási eredményeket a Rocq tételbizonyító rendszerben is formalizáljuk.