Syntactic Type Soundness in Structured Imperative Languages
| Authors | |
|---|---|
| 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 | |
| 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: |