Original title:
Typový systém pro sledování nebezpečných vedlejších efektů
Translated title:
A type system for tracking of unsafe side effects
Authors:
Beneš, Jiří ; Bednárek, David (advisor) ; Šefl, Vít (referee) Document type: Master’s theses
Year:
2022
Language:
eng Abstract:
[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
Keywords:
programming languages|type systems; programovací jazyky|typové systémy
Institution: Charles University Faculties (theses)
(web)
Document availability information: Available in the Charles University Digital Repository. Original record: http://hdl.handle.net/20.500.11956/174279