Pokročilé typové systémy
| Název práce v češtině: | Pokročilé typové systémy |
|---|---|
| Název v anglickém jazyce: | Advanced Type Systems |
| Klíčová slova: | funkcionální programování, typové systémy |
| Klíčová slova anglicky: | functional programming, type systems |
| Akademický rok vypsání: | 2015/2016 |
| Typ práce: | disertační práce |
| Jazyk práce: | |
| Ústav: | Katedra softwaru a výuky informatiky (32-KSVI) |
| Vedoucí / školitel: | doc. RNDr. Tomáš Dvořák, CSc. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 03.10.2016 |
| Datum zadání: | 03.10.2016 |
| Datum potvrzení stud. oddělením: | 06.10.2016 |
| Konzultanti: | RNDr. Jan Hric |
| Zásady pro vypracování |
| Typové systémy v informatice slouží jako syntaktické nástroje pro zajištění jisté míry abstrakce v programovacích jazycích [6]. Mezi hlavní funkce poskytované typovým systémem patří typová kontrola programů, která umožňuje detekci neplatného kódu a současně poskytuje údaje pro efektivní optimalizaci, typy mají ovšem i další využití: ve více expresivních systémech mohou sloužit též jako forma dokumentace [4,5].
Cílem práce je prozkoumat jak nové typové systémy, tak nové možnosti aplikace stávajících typových systémů v programovacích jazycích, se zaměřením na jazyky funkcionální a multiparadigmatické. Pozornost zasluhují zejména typové systémy se závislými typy a jejich role v intuicionistické a homotopické teorii typů [2] jakož i využití ve vysoce expresivních jazycích pro verifikaci programů (Coq [7], Agda [1]), konstrukce, které jsou možné pouze v takto silných jazycích (induktivní či koinduktivní datové typy, typová univerza) a využití teorie kategorií v jazycích s těmito typovými systémy. |
| Seznam odborné literatury |
| [1] Agda: An Interactive Proof Editor, http://wiki.portal.chalmers.se/agda/pmwiki.php
[2] Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, Princeton, NJ, 2013. [3] C. McBride, The derivative of a regular type is its type of one-hole contexts, http://strictlypositive.org [4] B. C. Pierce, Types and Programming Languages, MIT Press, Cambridge, MA, 2002 [5] B. C. Pierce, Advanced Topics in Types and Programming Languages, MIT Press, Cambridge, MA, 2005 [6] J. C. Reynolds, Types, abstraction and parametric polymorphism, Proceedings of the IFIP 9th World Computer Congress (Paris, September 19–23, 1983), pp. 513–523. [7] The Coq Proof Assistant, https://coq.inria.fr |
| Předběžná náplň práce |
| Pokročilé typové systémy a jejich využití ve funkcionálních a multiparadigmatických programovacích jazycích. |
| Předběžná náplň práce v anglickém jazyce |
| Advanced type systems and their uses in functional and multi-paradigm programming languages. |