Syntactic Type Soundness in Structured Imperative Languages

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Syntaktické odvození vlastnosti "Type soundness" ve strukturovaných imperativních jazycích
Autoři	MLNAŘÍK Hynek
Rok publikování	2007
Druh	Článek ve sborníku
Konference	MEMICS 2007: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	MEMICS
Obor	Informatika
Klíčová slova	type soundness; imperative languages; language IPL
Popis	Článek popisuje obecný způsob, jak prokázat vlastnosti "type soundness" ve strukturovaných imperativních jazycích. Tento způsob je ukázán na jednoduchém jazyku IPL. Program v tomto jazyce je množina funkcí. Abychom ukázali "type soundness", definujeme aproximativní syntaktický predikát, který staticky ověřuje korektnost funkce. Prezentovaný výsledek je vedlejší produkt vývoje kvantového jazyka LanQ, kde je využit pro prokázání vlastnosti "type soundness" tohoto jazyka. Přesto je možné tento postup použít v mnoha jiných existujících jazycích.
Související projekty:	Vysoce paralelní a distribuované výpočetní systémy Výpočty, komunikace a bezpečnost kvantových distribuovaných systémů