Ing. Ondřej Ryšavý, Ph.D.
|
| Hlavní řešitel: | Kolář Dušan, Škarvada Libor |
| Spoluřešitelé: | Peterka Ondřej, Ryšavý Ondřej |
| Agentura: | GAČR |
| Kód: | GA201/09/1316 |
| Začátek: | 2009 |
| Konec: | 2009 |
| Soubory: | |
|---|
|
| | Klíčová slova: | hodnotově-závislé typy; formální odvozování; funkcionální programování; lambda kalkul; jazykové konstrukce; objektový kalkul; objektová-orientace; specifikace a ověřování programů; teorie typu; |
| Anotace: |
| Pokročilá typová kontrola dokáže zajistit vyšší míru správnosti programu než je tomu běžné u současných programovacích jazyků. V některých případech použití takového systému znamená změnu přístupu k programování obecně. Navrhovaný projekt se zabývá základním výzkumem v oblasti typové kontroly pro objektově-orientovaný programovací jazyk, který by umožnil odhalovat vyšší množství chyb, kontrolovat složitější jazykové konstrukce a podporovat konstrukci korektních programů. Přístup k řešení naznačuje předpokládaný přínos projektu. Jedná se zejména o nalezení pozice hodnotově závislých typu v objektově-orientovaném typovaném prostředí. Vztah závislých typů, podtypů a objektových typů a studium vlastností takto definovaného systému včetně jeho vztahu k původní teorii jsou hlavní teoretické části projektu. K projektu pak také patří konstrukce experimentálního programovacího jazyka demonstrující studované vlastnosti. |
Publikace
| 2009 | Kollár Matej, Peterka Ondřej, Ryšavý Ondřej, Škarvada Libor: A Calculus of Coercive Subtyping, Brno, CZ, MUNI, 2009, s. 17 |
| | Škarvada Libor, Peterka Ondřej, Ryšavý Ondřej, Kolář Dušan: A Calculus of Coercive Subtyping, In: Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages, South Orange, US, SHU, 2009, s. 182-192 |
|
|