|
|
ParsecCore: A parser combinator library in the C# language
Tichý, Michal ; Kliber, Filip (advisor) ; Šefl, Vít (referee)
In this thesis, we implement a parser combinator library in C# inspired by Parsec. Parser combinators refer to a style of parsing where a parser is modeled as function from string to some structured result. Afterward, higher-order functions called combinators are used to combine simple parsers into more complex ones. Other such libraries exist, but in our estimation, they contain various deficiencies. We create an implementation without these faults and also introduce two new modules for parsing indentation- sensitive languages and permutations. We additionally implement two ex- ample parsers to showcase our library.
|
|
|
A type system for tracking of unsafe side effects
Beneš, Jiří ; Bednárek, David (advisor) ; Šefl, Vít (referee)
The current mainstream programming languages do not explicitly track side effects of the programs, such as the possibility of allocating memory, throwing an exception, and performing I/O actions. We create a fully speci- fied, novel type system based on graded comonads which can express opt-in, granular safety by annotating expressions which are safe with respect to a set of side effects. The advantages of granular safety are demonstrated using a proof-of-concept practical implementation which allows user-specified side effects tracked by our system. 1
|
|
|
Additive Pairs in Quantitative Type Theory
Svoboda, Tomáš ; Šefl, Vít (advisor) ; Kratochvíl, Miroslav (referee)
Both dependent types and linear types have their desirable properties. Department types can express functional dependencies of inputs and outputs, while linear types offer control over the use of computational resources. Combining these two systems have been difficult because of their different interpretations of context presence of variables. Quantitative Type Theory (QTT) combines dependent types and linear types by using a semiring to track the kind of use of every resource. We extend QTT with the additive pair and additive unit types, express the complete QTT rules in bidirectional form, and then present our interpreter of a simple language based on QTT. 1
|
|
|
Type inference and polymorphism for C
Klepl, Jiří ; Kratochvíl, Miroslav (advisor) ; Šefl, Vít (referee)
The C language, despite its age, is one of the main languages in systems development. It is valued for giving the user almost complete control over the memory management and the computations the program written in it performs. However, a large portion of criticism of C arises from the lack of generic programming features. C compensates that by utilizing preprocessor macros, which are prone to user errors. This problem has been addressed in the early stages of the development of the C++ language, but many systems developers refuse C++ because of its complexity and non-transparency of the code. We propose a simpler solution by applying the Hindley-Milner type sys- tem extended by Haskell type classes and type constructors. We will show that this approach is viable even with minimal changes to the syntax of C, but giving it much higher expressiveness. 1
|
|
|
C++ linter based on linear types
Beneš, Jiří ; Kratochvíl, Miroslav (advisor) ; Šefl, Vít (referee)
Low-level programming requires careful management of system resources, most notably memory. In C++ programmers are encouraged to follow idioms like RAII and smart pointers to handle resources correctly as violating them leads to unsafe code. Typed functional programming languages guarantee safe automatic mem- ory management, but are often sub-optimal in handling system resources. A nice, formal solution to handling resources naturally is linear types. Unfortu- nately, existing languages that support linearity are cumbersome and require explicit, complicated annotations from the programmer. We bridge the two worlds by exploring a novel combination of C++ and linear types. We describe a new type system with linearity for C++ by using constrained qualified types, while requiring no additional input from the programmer. The applied result of our work is called Lily, a static analysis tool for C++ using the Clang compiler infrastructure. Lily can statically detect large, general classes of issues, some of which are not detected by common state-of-the-art tools for C++. 1
|
|
|
OCR for tabular data
Tódová, Lucia ; Kratochvíl, Miroslav (advisor) ; Šefl, Vít (referee)
Table recognition is an important tool for digitalizing documents that con- tain tabular data, which often occur in areas of administration, finances and education. This thesis re-uses existing optical character recognition software to construct a new table recognition algorithm that aims to simplify the digitaliza- tion of diverse document types. The resulting algorithm achieves comparable or better results than currently available open-source software. Thesis additionally reviews common methods of OCR software implementation, and measures the influence of image preprocessing quality on the outcome of the table recognition. 1
|
|
|
Pattern recognition for in-game spell systems
Mikuš, Pavel ; Kratochvíl, Miroslav (advisor) ; Šefl, Vít (referee)
Magic is a popular element in current computer games. Although most games spoil the sensation of magic as of something extraordinarily subtle by allowing the player to cast spells by simply hitting key combinations, several games require the player to finish a more complicated action before casting a spell: Drawing a complicated glyph that represents the spell is one of such actions. This thesis aims to provide a repurposable library that would allow simple implementation of structured glyph-drawing-based in-game spell systems. The thesis studies several relevant approaches to pattern recognition, describes a neural-network based method for recognition of various shapes and shape combinations, develops a system for describing the parameters and results of the used algorithm in terms of predefined spell shapes and their recognized combinations, and implements this approach in a library and an accompanying simple demonstrational game. The library and its parameters are benchmarked and systematically optimized.
|
|
|
λ-calculus as a Tool for Metaprogramming in C++
Šefl, Vít ; Hric, Jan (advisor) ; Kratochvíl, Miroslav (referee)
The template system of C++ is expressive enough to allow the programmer to write programs which are evaluated during compile time. This can be exploited for example in generic programming. However, these programs are very often hard to write, read and maintain. We introduce a simple translation from lambda calculus into C++ templates and show how it can be used to simplify C++ metaprograms. This variation of lambda calculus is then extended with Hindley-Milner type system and various other features (Haskell-like syntax, user-defined data types, tools for interaction with existing C++ template code and so on). We then build a compiler capable of transforming programs written in this language into C++ template metaprograms. Powered by TCPDF (www.tcpdf.org)
|
|
|
Comonads (not only) for programmers
Šefl, Vít ; Hric, Jan (advisor) ; Pultr, Aleš (referee)
Monads (and their categorical dual - comonads) are important concepts in category theory and while monads enjoy their popularity in functional languages (mainly due to the programming language Haskell), comonads are often forgotten. In this work we present a definition of comonads suitable for programming and give examples of their use. One of the more important examples is zipper - a structure used to represent position. We show that zipper can be automatically derived for any regular type and show that this operation is very reminiscent of derivative from mathematical analysis. We also show worked examples of various problems that comonads can help solve in the language Haskell. All relevant proofs for the theoretical part of this work are machine checked in the language Agda. Powered by TCPDF (www.tcpdf.org)
|
guest ::
