Syntactic Type Soundness in Structured Imperative Languages

Warning

This publication doesn't include Faculty of Medicine. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	MLNAŘÍK Hynek
Year of publication	2007
Type	Article in Proceedings
Conference	MEMICS 2007: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
MU Faculty or unit	Faculty of Informatics
Citation
Web	MEMICS
Field	Informatics
Keywords	type soundness; imperative languages; language IPL
Description	We present a general technique for proving type soundness of a structured imperative programming language. We show this technique on a simple language IPL. A program in the language is a set of functions. To prove type soundness we develop an approximate syntactic predicate that statically checks function correctness. The presented result is a byproduct of the development of a quantum programming language LanQ where it was used to prove type soundness. Nevertheless, it is applicable to a wide range of other existing classical languages.
Related projects:	Highly Parallel and Distributed Computing Systems Quantum multipartite computation, communication and security