Publication details

Syntactic Type Soundness in Structured Imperative Languages

Investor logo


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

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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info