|
|
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.