Studying the ML module system in HOL

Elsa Gunter, Savi Maharaj

Research output: Contribution to journalArticlepeer-review


In an earlier project of VanInwegen and Gunter, the dynamic semantics of the Core of Standard ML (SML) was encoded in the HOL theorem-prover. We extend this by adding the dynamic Module system. We then develop a possible dynamic semantics for a Module system with higher-order functors and encode this as well. Next we relate these two semantics via embeddings and projections and discuss how we use these to prove that evaluation in the proposed system is a conservative extension, in an appropriate sense, of evaluation in the SML Module system.

Original languageEnglish (US)
Pages (from-to)142-151
Number of pages10
JournalComputer Journal
Issue number2
StatePublished - 1995
Externally publishedYes

ASJC Scopus subject areas

  • Computer Science(all)

Cite this