Supporting Formal Reasoning about Standard ML

Graham Collins and Stephen Gilmore

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.

LFCS report ECS-LFCS-94-310, November 1994.

Previous | Index | Next