Detail práce
Just-in-Time Compilation of Dependently-Typed Lambda Calculus
Řada programovacích jazyků byla schopna zvýšit svoji rychlost výměnou běhových systémů stavěných na míru za obecné platformy, které pro optimalizaci používají just-in-time překlad, jako jsou GraalVM nebo RPython. V této práci vyhodnocuji, zda je použití takovýchto platforem vhodné i pro jazyky se závislymi typy nebo důkazovými systémy.
Tato práce představuje koncepty -kalkulu a teorie typů potřebné pro úvod do závislých typů s relevantními algoritmy, specifikuje malý závisle typovaný jazyk založený na $\lambda\Pi$ kalkulu, a prezentuje dva interpretery tohoto jazyka. Tyto interpretery jsou psané v jazyce Kotlin, první je jednoduchý, psaný ve funkcionálním stylu a druhý používá platformu GraalVM a Truffle. GraalVM je platforma založená na virtuálním stroji Javy (JVM), která přidává just-in-time překladač založený na částečném vyhodnocení (partial evaluation) a Truffle je knihovna pro tvorbu programovacích jazyků využívající tento překladač. Závěr práce vyhodnocuje běhové charakteristiky těchto interpreterů na různých zátěžových testech.Závěry práce jsou ale silně negativní. Vliv JIT překladu není znatelný ani přes snahu optimalizovat běžné algoritmy z teorie typů, které jsou zjevně nevhodné pro platformu JVM. Práce končí návrhy několika navazujících projektů, které by lépe využily možnosti Truffle a které by byly vhodnější pro implementaci závisle typovaných jazyků.
Truffle, Virtuální stroj JVM, just-in-time překlad, tvorba překladačů, závislé typy
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm B.
- Můžete diskutovat případnou možnost praktické využitelnosti práce?
- Vypořádáváte se nějak s ověřováním terminace?
- Můžete prosím ještě jednou vysvětlit graf na slidu 9?
- Proč jste vaši práci nekonzultoval častěji s vedoucím?
- Proč je u vašeho řešení důležitá rychlost?
Hradiš Michal, Ing., Ph.D. (UPGM FIT VUT), člen
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT24198,
author = "Jakub Z\'{a}rybnick\'{y}",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Just-in-Time Compilation of Dependently-Typed Lambda Calculus",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2021,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/24198/"
}