登入
選單
返回
Google圖書搜尋
Supporting Formal Reasoning about Standard ML
Graham Collins
Stephen Gilmore
University of Edinburgh. Laboratory for Foundations of Computer Science
出版
LFCS, Department of Computer Science, University of Edinburgh
, 1994
URL
http://books.google.com.hk/books?id=fF88PwAACAAJ&hl=&source=gbs_api
註釋
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."
