Original title: Pokročilé typové systémy
Translated title: Advanced Type Systems
Authors: Šefl, Vít ; Dvořák, Tomáš (advisor)
Document type: Rigorous theses
Year: 2025
Language: eng
Abstract: [eng] [cze]
While the results of type system research are being incorporated into many main- stream programming languages, this process has generally been conservative and slow. Recent research results have the potential to greatly increase the expressiveness of their type systems. This thesis demonstrates the application of three such results in practical programming: the use of a polymorphic lambda calculus to eliminate errors in template metaprograms, the efficiency of zippers obtained through algebraic data type differen- tiation, and practical uses of additive types in substructural type theories. We further demonstrate the viability of the proposed solutions by defining and implementing two new programming languages, as well as providing a detailed performance analysis of zippers and their imperative counterparts. Ačkoliv se výsledky výzkumu typových systémů postupně přidávají do běžných pro- gramovacích jazyků, tento proces je obvykle konzervativní a pomalý. Nejnovější výsledky v této oblasti by mohly značně vylepšit expresivitu běžných typových systémů. Tato práce demonstruje využití třech konkrétních výsledků v praktickém programování: použití po- lymorfního lambda kalkulu na eliminaci chyb v šablonových metaprogramech, efektivitu zipperů definovaných pomocí derivace algebraických datových typů a praktické použití aditivních typů ve substrukturálních typových teorií. Pro ukázku proveditelnosti navrže- ných řešení je součastí práce taktéž definice a implementace dvou nových programovacích jazyků a podrobná analýza výkonu zipperů a jim podobných datových struktur.
Keywords: functional programming; type systems; funkcionální programování; 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/204864

Permalink: http://www.nusl.cz/ntk/nusl-691451


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Rigorous theses