Type System - A Formal Method Formal Tool for Programming Languages

摘要

We take type system as a formal method and a formal tool for programming language. It can be built in the early stage of language development served as a formal method in order to design and implement the language with rigorousness, precision and correctness. It can also be built as a formal tool for language analysis to get the mathematical properties after the language has come into being. In this paper, the most important and basic characteristics of type system have been discussed. And by the introduction of the type system of a graph-based functional language SClean, a practical method has been given on how to construct and implement an actual type system of an actual programming language, which is hoped to be of practical usefulness.