Pokročilé typové systémy

• Thesis title in Czech: Pokročilé typové systémy
• Thesis title in English: Advanced Type Systems
• Key words: funkcionální programování, typové systémy
• English key words: functional programming, type systems
• Academic year of topic announcement: 2015/2016
• Thesis type: dissertation
• Department: Department of Software and Computer Science Education (32-KSVI)
• Supervisor: doc. RNDr. Tomáš Dvořák, CSc.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 03.10.2016
• Date of assignment: 03.10.2016
• Confirmed by Study dept. on: 06.10.2016
• Advisors: RNDr. Jan Hric

Guidelines

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.

References

[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

Preliminary scope of work

Pokročilé typové systémy a jejich využití ve funkcionálních a multiparadigmatických programovacích jazycích.

Preliminary scope of work in English

Advanced type systems and their uses in functional and multi-paradigm programming languages.