Automating Type Soundness Proofs via Decision Procedures and Guided
Reductions (PDF preprint, missing diagram). With Andy Gordon.   Postscript with diagram, but which does not seem to display correctly in Ghostview is here (i.e. needs to be printed). 

Operational models of fragments of the Java Virtual Machine and the .NET Common Language Runtime have been the focus of considerable study in recent years, and of particular interest have been specifications and machine-checked proofs of type soundness. In this paper we aim to increase the level of automation used when checking type soundness for these formalizations. We present a semi-automated technique for reducing a range of type soundness problems to a form that can be automatically checked using a decidable first-order theory. Deciding problems within this fragment is exponential in theory but is often efficient in practice, and the time required for proof checking can be controlled by further hints from the user. We have applied this technique to two case studies, both of which are type soundness properties for subsets of the .NET Common Language Runtime. These case studies have in turn aided us in our informal analysis of that system.

Don Syme, dsyme@microsoft.com , Microsoft Research, Cambridge 

Work (+44) 1223 744797, fax (+44) 1223 744 777