Abstract: A set of tools to support reasoning about Standard ML is described. These tools are based on the ML Kit compiler and the HOL-ML embedding of the dynamic semantics of Standard ML within the HOL90 interactive proof system. Examples are developed showing the use of these tools in reasoning about simple Standard ML program fragments.
Previous | Index | Next An error occured whilst processing this directive