The theory of programming languages is one of the core areas of computer sicence offering a wealth of models and methods. Yet the complexity of most real programming languages means that a complete formalization of their semantics is only on limited use unless it is supported by mechanical means for reasoning about the formalization. This line of research started in earnest with the seminal paper by Gordon [1] who defined the semantics of a simple while-language in the HOL system and derived Hoare logic from the semantics. Since then, and ever growing number of more and more sophisticated programming languages have been embedded in theorem provers.
展开▼
