Myra Vanlnwegen, Elsa Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We describe here HOL-ML, an encoding of a subset of SML and its dynamic semantics (as described by The Definition of Standard ML) in HOL. This encoding, which is the first stage in a project that will include typechecking and SML Modules, allows the formal study of the evaluation of a real programming language including state and control constructs (exceptions). In this paper we describe the subset of SML that we encoded and the semantic objects needed for its evaluation. We explain how we defined the evaluation rules and how we proved that evaluation is deterministic. We describe briefly the next step, which is to define a larger language that includes type declarations and to define the typechecking rules on it. Finally, we give a short description of the mutually recursive type definition package that we wrote to enable us to define the types we needed to create the HOL-ML grammar.

Original languageEnglish (US)
Title of host publicationHigher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
EditorsJeffrey J. Joyce, Carl-Johan H. Seger
Number of pages14
ISBN (Print)9783540578260
StatePublished - 1994
Externally publishedYes
Event6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 - Vancouver, Canada
Duration: Aug 11 1993Aug 13 1993

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume780 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'HOL-ML'. Together they form a unique fingerprint.

Cite this