Formalising Strong Normalisation Proofs of the Explicit Substitution Calculi in ALF1

[摘要] Explicit substitution calculi have become very fashionable in the last decade. The reason is that substitution calculi bridge theory and implementation and enable control over evaluation steps and strategies. Of the most important questions of explicit substitution calculi is that of the termination of the underlying calculus of substitution. For this reason, one finds with every new calculus of explicit substitution, a section devoted to the termination of substitutions. Those proofs of termination fall under two categories. Proofs that are easy because a decreasing measure can be established and proofs that are difficult because such a decreasing measure is not easy to establish. Another fashionable subject has been the checking of proofs using a proof checker. This is useful because some proofs can be intricate and hard to believe if they are not proof checked. This thesis investigates the methods to prove termination of explicit substitution calculi and their formalisations in the proof checker ALF. Two styles of explicit substitution calculi are chosen for this purpose, one is the calculus s whose termination is guaranteed by a decreasing weight, the other is the calculus a whose termination is extremely complex. Two new termination proofs of the calculus s are given. All termination proofs of both s and a presented in the thesis are formalised in ALF. During our process of formalisations we comment on what is needed to make a proof checkable during the checking process.

[发布机构] University:University of Glasgow

[关键词] Computer science