Název:
Typový systém pro sledování nebezpečných vedlejších efektů
Překlad názvu:
A type system for tracking of unsafe side effects
Autoři:
Beneš, Jiří ; Bednárek, David (vedoucí práce) ; Šefl, Vít (oponent) Typ dokumentu: Diplomové práce
Rok:
2022
Jazyk:
eng
Abstrakt: [eng][cze] The current mainstream programming languages do not explicitly track side effects of the programs, such as the possibility of allocating memory, throwing an exception, and performing I/O actions. We create a fully speci- fied, novel type system based on graded comonads which can express opt-in, granular safety by annotating expressions which are safe with respect to a set of side effects. The advantages of granular safety are demonstrated using a proof-of-concept practical implementation which allows user-specified side effects tracked by our system. 1Mainstreamové programmovací jazyky si neuchovávají informace o vedlej- ších efektech programů, kterými jsou například možnost alokování paměti, vyhození výjimky a provádění akcí souvisejících se vstupem a výstupem. Vytvořili jsme plně specifikovaný, originální typový systém založený na stup- ňovitých komonádách, jenž dokáže vyjádřit opt-in, granulární bezpečnost oz- načením výrazů jazyka jakožto bezpečné vzhledem k dané množině vedlejších efektů. Výhody granulární bezpečnosti jsou demonstrovány pomocí praktické implementace, která umožňuje našemu systému sledovat uživatelem speci- fikované vedlejší efekty. 1
Klíčová slova:
programovací jazyky|typové systémy; programming languages|type systems