Syntactic Type Soundness in Structured Imperative Languages

Investor logo

Warning

This publication doesn't include Faculty of Arts. 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:

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