In her thesis, Kateřina Medková has produced a remarkable exposition of the foundations of linear logic, and a suprisingly deep and comprehensive survey of the existing literature on one of its most important applications, namely implicit computational complexity (ICC). In so doing, she has dramatically exceeded the expectations of the project proposal, and produced a document whose depth and breadth goes far beyond what I would expect from a Bachelor thesis.

Linear logic first appeared in the 1970s in work of Girard, as a formal system more closely tied to the needs of theoretical computer science than the prevailing classical or intuitionistic proof systems. The difference lies in the way that propositions are treated: in linear logic they are regarded as resources to be used or produced, and each occurrence must be carefully accounted for. Formally, this amounts to the stripping of the bookkeeping-free rules of inference in classical or intuitionistic logic, namely weakening and contraction. The shift in perspective also forces the familiar logical connectives to split into internal and external variants, further complicating the story. It could be said that the field developed too rapidly: the foundational literature contains much confusion, and many terminological and conceptual conflicts. Thankfully, Ms. Medková has managed to synthesise all of this information in Part I of the thesis, resulting in a comprehensive and lucid exposition of linear logic, with both technical details and intuitive explanations provided.

The second portion of the thesis is concerned with ICC and, specifically, the way in which particular fragments of linear logic allow us to code familiar algorithmic complexity classes, e.g. P, k-EXP, and so on. Work in ICC aims to provide intrinsic characterisations of complexity classes: rather than looking at algorithms from the outside and measuring steps required in terms of input size, or reducing to algorithms whose complexity is already understood, one actually restricts the operations available to ensure that one stays in the given class. This can involve the specification of programming languages in which only programs of a given class can be produced, or, one step removed, captured by a formal system via the Curry-Howard isomorphism. In the latter version, programs are associated with proofs in the formal system, and executions with proof normalisations---essentially, simplifications of a given proof to avoid any unnecessary hypotheses. Complexity then corresponds precisely to complexity of proof normalisations. By restricting to particular fragments of linear logic, one can tune the complexity of proof normalisation to match that of the desired class, as Ms. Medková explains in Part II, and summarises in the conclusion of the thesis.

The thesis reflects a highly sophisticated understanding of these complex notions, and is structured in such a way as to allow a careful reader with some logical background to arrive at a surprisingly deep understanding both of linear logic itself and of its applications to ICC. Judicious choices are made as to what to include, the order in which subjects should be presented, and how to explain them to greatest effect. There are places where certain technical notions that would be useful to see in greater detail must be replaced by intuitive explanations, but this is to be expected. Individual chapters are carefully connected to produce a unified account. The student is to be commended, too, for her independence and professional approach: she quickly digested any source I recommended, and has read far, far more. During regular meetings, she arrived with lengthy lists of detailed questions and, when otherwise reachable, was highly responsive to suggestions for improvement.

As a final note: there is little to no literature on linear logic in Czech, and none I have found that goes into the depth of Ms. Medková's thesis. This, along with the comprehensive Czech-English glossary of terms she has produced, represents a real contribution to the dissemination of these important ideas.

Práce se zabývá lineární logikou a jejími aplikacemi v teorii výpočetní složitosti. Autorka si vytkla ambiciózní cíl představit základní principy lineární logiky, její důkazově-teoretické aspekty a ukázat souvislosti s moderní teoretickou informatikou. Tento cíl byl splněn. Text je přehledně strukturován, logicky navazuje od úvodních pojmů klasické logiky, sekventového kalkulu a Curryho–Howardovy korespondence až k pokročilejším tématům, jako jsou důkazové sítě, Bounded Linear Logic, Light Linear Logic či Elementary Linear Logic.

Jedná se o náročné téma, studentka jej však dokázala zvládnout v širokém rozsahu a dát do souvislosti různé typy odvozených logik s problémy teoretické informatiky jako je složitost či vyčíslitelnost. V  závěru uvádí významnou větu, která tyto disciplíny přímo propojuje. Práce je založena na studiu odborné literatury, kterou autorka vhodně využívá k odkazu na důležitá tvrzení, která dále zasazuje do širšího kontextu. Oceňuji také přehledně zpracovaný Apendix, kde je popsána sémantika lineární logiky a slovník pojmů. Po formální i jazykové stránce je zpracována na velmi dobré úrovni. Práce splňuje zadání v plném rozsahu a prokazuje schopnost samostatně nastudovat a zpracovat náročné matematické téma.
Připomínek nemám mnoho, zmíním aspoň jednu. Curryho–Howardova korespondence je zavedena jako izomorfismus, což matematicky smýšlejícího čtenáře vede k očekávání bijekce mezi množinami, této úrovní podrobnosti se však prezentace tohoto pojmu vyhýbá - zjevně jde o standardní formu. 
Práci doporučuji ji k obhajobě s hodnocením A. Topics for thesis defence:

1. Interpretace modality ! je vysvětlena jako neomezené užití. Jaká je interpretace exponenciálních spojek ? a !! (konec otázky, otazník by ji změnil)
2. Uveďte nějaké příklady důkazových struktur nebo důkazového boxu. Nejlépe jednu strukturu, která je sítí a jednu, která důkazovou sítí není.