|
|
Combining effects with dependent types
Mückenschnabel, Maya ; Petříček, Tomáš (vedoucí práce) ; Šefl, Vít (oponent)
Dependent type systems provide a novel way of reasoning about program correctness, by embedding behavior of the program into the more expressive type system. Correctness is achieved by not allowing incorrect states to be representable. Languages like Idris show that dependent type systems are practically useful, not only for formal proofs, but also for creating fewer bugs in production. But the purity of computation poses a problem for composability of stateful computations and of side effects. Effect handlers provide one possible solution for this problem. In this thesis we propose an effect extension of depen- dent type systems. The resulting system not only makes it possible to provide guarantees about correctness of a program, but also make it easy to compose such guarantees using effects. We formalize the type system and present a prototype implementation.
|
|
|
ParsecCore: A parser combinator library in the C# language
Tichý, Michal ; Kliber, Filip (vedoucí práce) ; Šefl, Vít (oponent)
V této práci implementujeme parsovací knihovnu pro C# inspirovanou Parsecem, která využívá parsovací kombinátory. Parsovací kombinátory od- kazují na styl syntaktické analýzy, při kterém je parser modelován jako funkce, která bere textový řetězec jako vstup a produkuje strukturovaný výsledek. Následně používáme funkce vyšších řádů, kterým se říká kombi- nátory, pro spojování jednoduchých perserů do komplexnějších. Knihovny založené na stejném principu již existují, avšak, v našem mínění, jsou v ně- kterých ohledech nedostačující. Naše implementace nemá tyto nedostatky a také obsahuje dva nové moduly, které pomáhají se syntaktickou analýzou jazyků, pro které odsazení je signifikantní, a také se syntaktickou analýzou permutací. Dále implementujeme dva příkladné parsery, abychom předvedli naši knihovnu.
|
|
|
A type system for tracking of unsafe side effects
Beneš, Jiří ; Bednárek, David (vedoucí práce) ; Šefl, Vít (oponent)
Mainstreamové 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
|
|
|
Additive Pairs in Quantitative Type Theory
Svoboda, Tomáš ; Šefl, Vít (vedoucí práce) ; Kratochvíl, Miroslav (oponent)
Jan závislé, tak lineární typy mají své kýžené vlastnosti. Zatímco závislé typy mo- hou vyjádřit závislosti mezi vstupy a výstupy funkcí, lineární typy umožňují kontrolu nad používáním zdrojů. Kombinace těchto dvou systémů byla složitá kvůli dvou různým interpretacím výskytu proměnné v kontextu. Teorie kvantitativních typů (QTT) kom- binuje závislé a lineární typy použitím polookruhů ke sledování druhů spotřeby každé proměnné. Tato práce rozšiřuje QTT o aditivní páry a aditivní jednotky, formuluje kompletní QTT pravidla ve formě oboustranného typování, a prezentuje náš interpret jednoduchého jazyka založeného na QTT. 1
|
|
|
Typová inference a polymorfismus pro jazyk C
Klepl, Jiří ; Kratochvíl, Miroslav (vedoucí práce) ; Šefl, Vít (oponent)
Jazyk C, i přes své stáří, stále patří mezi přední jazyky programování počítačových systémů. Jeho ceněnou přednosti je, že uživateli poskytuje takřka úplnou kontrolu nad správou paměti a nad prováděnými výpočty. C však snáší kritiku za to, že v něm chybí prvky umožňující generické programování, což se v C kompenzuje používáním preprocesorových maker, což zvyšuje náchylnost na uživatelské chyby. Tento problém již řeší jazyk C++ už od počátků svého vývoje, ale spousta vývojářů počítačových systémů jej odmítá pro jeho komplexitu a netranspar- entnost kódu. Předkládáme tedy návrh na jednodušší řešení užitím typového systému Hindley-Milner. Toto řešení pak jen za drobých úprav syntaxe jazyka C poskytne mnohem vyšší expresivitu jazyka. 1
|
|
|
C++ linter based on linear types
Beneš, Jiří ; Kratochvíl, Miroslav (vedoucí práce) ; Šefl, Vít (oponent)
Nízkoúrovňové programování vyžaduje opatrnou práci se systémovými zdroji, hlavně s pamětí. Programátoři v C++ používají ustálené zásady jako RAII a chytré ukazatele ke korektní práci se zdroji. Porušení podobných zásad vede často k nebezpečnému kódu. Funkcionální programovací jazyky s typy garantují bezpečnou a automat- ickou správu paměti, ale jejich práce se systémovými zdroji je často subop- timální. Hezký, formální prostředek k práci se zdroji jsou lineární typy. Bo- hužel, existující jazyky podporující linearitu jsou složité a vyžadují explicitní anotace od programátora. Prozkoumáváme propojení těchto světů pomocí kombinace C++ a lineárních typů. V práci popisujeme nový typový systém s linearitou pro C++ použitím omezených kvalifikovaných typů, bez požadavku na součinnost programá- tora. Aplikovaný výsledek naší práce je Lily, nástroj pro statickou analýzu C++ používající infrastrukturu překladače Clang. Lily umí staticky deteko- vat velké, obecné třídy problémů, z nichž některé nejsou detekované jinými běžně používanými nástroji pro C++. 1
|
|
|
OCR for tabular data
Tódová, Lucia ; Kratochvíl, Miroslav (vedoucí práce) ; Šefl, Vít (oponent)
Rozpoznávanie tabuliek je dôležitým nástrojom pre digitalizáciu tabu- ľkových dokumentov, ktoré sa bežne využívajú v oblastiach administratívy, bankovníctva a vzdelávania. Cieľom práce je za pomoci existujúceho soft- véru na optické rozpoznávanie znakov (OCR) implementovať nový algoritmus na rozpoznávanie tabuliek pre zjednodušenie digitalizácie rôznorodých doku- mentov. V porovnaní s dnešnými open-source softvérmi dosahuje výsledný algoritmus porovnateľné alebo lepšie výsledky. Práca navyše dokumentuje rôzne implementácie OCR a meria vplyv kvality predspracovania obrázku na rozpoznávanie tabuliek.
|
|
|
Pattern recognition for in-game spell systems
Mikuš, Pavel ; Kratochvíl, Miroslav (vedoucí práce) ; Šefl, Vít (oponent)
Magie tvoří v současných hrách populární element. Nicméně většina her kazí pocit z magie jakožto něčeho jedinečného, tím, že hráči umožní kouzlit pouhým stiskem několika kláves. Jsou však i hry vyžadují složitější mechanismus kouzlení, a právě kreslení komplexních symbolů je jedním z nich. Cílem této práce je nabídnout opakovatelně použitelnou knihovnu umožňující jednoduchou implementaci strukturovaného herního systému kouzel, založeného na kreslení symbolů. Práce zkoumá několik relevantních přístupů k rozpoznávání vzorů, popisuje metodu využívající neurální sítě k rozpoznání různých tvarů a jejich kombinací, vytváří systém pro popis parametrů a výsledků použitých algoritmů v rámci předdefinovaných tvarů kouzel a jejich rozpoznaných kombinací a implementuje tento přístup do knihovny a jednoduché doprovodné demonstrační hry. Knihovna a její parametry jsou porovnávány a systematicky optimalizovány.
|
|
|
λ-calculus as a Tool for Metaprogramming in C++
Šefl, Vít ; Hric, Jan (vedoucí práce) ; Kratochvíl, Miroslav (oponent)
Šablonový systém jazyka C++ je natolik expresivní, že umožňuje napsat programy, které se vyhodnocují již během kompilace. Toho se dá využít například v generickém programování. Tyto programy jsou ale často náročné na psaní, čtení i údržbu. Navrhneme proto jednoduchý překlad z lambda kalkulu právě do C++ šablon a ukážeme, jak jej lze využít pro zjednodušení takovýchto metaprogramů. K této variantě lambda kalkulu dále přidáme Hindley-Milnerovo typový systém, Haskell syntaxi, uživatelsky definované datové typy, nástroje pro interakci se stávajícími šablonovými programy atp. Nakonec vytvoříme kompilátor, který je schopen transformovat programy psané v tomto jazyce do šablonových metaprogramů v C++. Powered by TCPDF (www.tcpdf.org)
|
|
|
Komonády (nejen) pro programátory
Šefl, Vít ; Hric, Jan (vedoucí práce) ; Pultr, Aleš (oponent)
Monády (a jejich kategorický duál - komonády) jsou důležitým konceptem teorie kategorií a zatímco monády jsou velmi oblíbenými nástroji ve funkcionálních jazycích (hlavně díky jazyku Haskell), komonády se příliš nepoužívají. V této práci prezentujeme definici komonád vhodnou pro potřeby funkcionálního programování a dále uvádíme příklady jejich praktického použití. Jedním z důležitějších příkladů je zipper - struktura, která reprezentuje určitou pozici. Ukážeme, že zipper lze automaticky odvodit pro každý regulární typ a také že tato operace připomíná derivaci z matematické analýzy. Kromě toho také uvádíme několik řešených příkladů v jazyce Haskell, které ilustrují, jak lze komonády použít pro řešení různých problémů. Všechny důkazy v teoretické části jsou provedeny v jazyce Agda a jsou zkontrolovány počítačem. Powered by TCPDF (www.tcpdf.org)
|
host ::
RSS.