Semi-automatic Verification of the Soundness of Type Systems.
Bachelor Thesis, Master Thesis
Type systems shall ensure that correctly typed programs do not get stuck during execution. More formally, type systems shall satisfy certain soundness criteria, for example, progress and preservation (see Pierce). However, proving the soundness of type systems by hand is a tedious and error-prone task. Therefore, it is desirable to have special tool-support for soundness proofs of type systems such that these proofs, or at least large parts of them, can be conducted automatically.
To this end, we have built a research prototype called Veritas that makes it possible for conducting progress and preservation proofs for type systems for simple programming languages (for example for the simply-typed lambda calculus) in a semi-automatic fashion: Main proof steps of the progress and preservation proofs can be stated within Veritas by hand and can be proven fully automatically by a first-order theorem prover.
In this thesis, the student candidate shall evaluate our semi-automatic approach for small extensions of the type system for the simply-typed lambda calculus with regard to the following questions: Is our semi-automatic approach also applicable for slightly more complex languages than the pure simply-typed lambda calculus? Which degree of automation does our current approach support under the presence of such extensions? Does the combination of different extensions generate interdependencies between extensions in the proof that require to be resolved manually?
- Benjamin C. Pierce: Types and Programming Languages. 2002