Název: Inferencí řízená správa zdrojů a polymorfismus pro systémové programování
Překlad názvu: Inference-driven resource managemenent and polymorphism in systems programming
Autoři: Klepl, Jiří ; Kratochvíl, Miroslav (vedoucí práce) ; Bednárek, David (oponent)
Typ dokumentu: Diplomové práce
Rok: 2022
Jazyk: eng
Abstrakt: [eng] [cze]
Systems programming languages facilitate the implementation of software that runs in restricted environments close to the hardware, such as operating systems, drivers, and real-time and embedded systems. Implementation of desirable features of such languages, such as generic programming and type system capabilities that prevent programmer errors, are complicated by strict constraints on the run-time properties of the program. This thesis explores a novel combination of C-- language with advanced type system features that allow type checking of highly polymorphic generic code and demonstrates type-driven resource management in this language. As the main result, the thesis provides a proof-of-concept in a prototype compiler of an extended ver- sion of C-- to LLVM and describes a type system based on deferred constraint solving that is capable of type inference in the presence of multi-parameter typeclasses and C-- subtypes. We demonstrate the functionality of the type system and the compiler on selected program examples and report several identified design challenges that may be addressed to make the system more practical. 1 Jazyky pro Systémové programování usnadňují implementaci softwaru, který běží v omezených prostředích blízko hardwaru, jako jsou operační sys- témy, drivery, systémy reálného času a vestavěné systémy. Implementace prospěšných prvků pro tyto jazyky, jako jsou generické programování a ty- pový systém zajišťující bezchybnost kódu, je ztěžována úzkými požadavky na běhovýmé vlastnostni programu. Hlavní náplní této práce je prozk- oumat novou kombinaci jazyka C-- s prvky typového systému umožňující typovou kontrolu vysoce polymorfního kódu a demonstruje možnosti typově vedené správy zdrojů v tomto jazyku. Jako hlavní výstup práce podává důkaz konceptu zprostředkovaný prototypem překladače rožšířeného jazyka C-- do LLVM a popisuje typový systém založený na odkládajícím řešení omezujících podmínek, který je schopen typové inference za přítomnosti více- parametrových typových tříd a subtypy C--. Funkcionalitu typového systému a překladače demonstrujeme na vybraných ukázkách programů a popisujeme několik rozpoznaných komplikací návrhu, které lze adresovat pro praktičtější implementaci. 1
Klíčová slova: programovací jazyky|typové systémy|kompilátory|systémové programování|správa zdrojů; programming languages|type systems|compilers|systems programming|resource management

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/176279

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-510378


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce