Advanced Type Systems

Šefl, Vít

Pokročilé typové systémy

dc.contributor.advisor	Dvořák, Tomáš
dc.creator	Šefl, Vít
dc.date.accessioned	2025-04-16T07:15:39Z
dc.date.available	2025-04-16T07:15:39Z
dc.date.issued	2025
dc.identifier.uri	http://hdl.handle.net/20.500.11956/197824
dc.description.abstract	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.	en_US
dc.description.abstract	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.	cs_CZ
dc.language	English	cs_CZ
dc.language.iso	en_US
dc.publisher	Univerzita Karlova, Matematicko-fyzikální fakulta	cs_CZ
dc.subject	functional programming	en_US
dc.subject	type systems	en_US
dc.subject	funkcionální programování	cs_CZ
dc.subject	typové systémy	cs_CZ
dc.title	Advanced Type Systems	en_US
dc.type	dizertační práce	cs_CZ
dcterms.created	2025
dcterms.dateAccepted	2025-03-26
dc.description.department	Katedra softwaru a výuky informatiky	cs_CZ
dc.description.department	Department of Software and Computer Science Education	en_US
dc.description.faculty	Faculty of Mathematics and Physics	en_US
dc.description.faculty	Matematicko-fyzikální fakulta	cs_CZ
dc.identifier.repId	177856
dc.title.translated	Pokročilé typové systémy	cs_CZ
dc.contributor.referee	Mycroft, Alan
dc.contributor.referee	Petříček, Tomáš
thesis.degree.name	Ph.D.
thesis.degree.level	doktorské	cs_CZ
thesis.degree.discipline	Theoretical Computer Science and Artificial Intelligence	en_US
thesis.degree.discipline	Teoretická informatika a umělá inteligence	cs_CZ
thesis.degree.program	Theoretical Computer Science and Artificial Intelligence	en_US
thesis.degree.program	Teoretická informatika a umělá inteligence	cs_CZ
uk.thesis.type	dizertační práce	cs_CZ
uk.taxonomy.organization-cs	Matematicko-fyzikální fakulta::Katedra softwaru a výuky informatiky	cs_CZ
uk.taxonomy.organization-en	Faculty of Mathematics and Physics::Department of Software and Computer Science Education	en_US
uk.faculty-name.cs	Matematicko-fyzikální fakulta	cs_CZ
uk.faculty-name.en	Faculty of Mathematics and Physics	en_US
uk.faculty-abbr.cs	MFF	cs_CZ
uk.degree-discipline.cs	Teoretická informatika a umělá inteligence	cs_CZ
uk.degree-discipline.en	Theoretical Computer Science and Artificial Intelligence	en_US
uk.degree-program.cs	Teoretická informatika a umělá inteligence	cs_CZ
uk.degree-program.en	Theoretical Computer Science and Artificial Intelligence	en_US
thesis.grade.cs	Prospěl/a	cs_CZ
thesis.grade.en	Pass	en_US
uk.abstract.cs	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.	cs_CZ
uk.abstract.en	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.	en_US
uk.file-availability	V
uk.grantor	Univerzita Karlova, Matematicko-fyzikální fakulta, Katedra softwaru a výuky informatiky	cs_CZ
thesis.grade.code	P
dc.contributor.consultant	Hric, Jan
uk.publication-place	Praha	cs_CZ
uk.thesis.defenceStatus	O