Skip header navigation
×

Conference Proceeding

Studying the ML module system in HOL

Citation
Maharaj S & Gunter EL (1994) Studying the ML module system in HOL. In: Melham T & Camilleri J (eds.) Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop Valletta, Malta, September 19–22, 1994 Proceedings. Lecture Notes in Computer Science, 859. 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Valletta, Malta, 19.09.1994-22.09.1994. Berlin Heidelberg: Springer, pp. 346-361. http://link.springer.com/chapter/10.1007/3-540-58450-1_53#; https://doi.org/10.1007/3-540-58450-1_53

Abstract
In an earlier project [5] 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 can use these to state and to prove that evaluation in the proposed system is a conservative extension, in an appropriate sense, of evaluation in the SML Module system.

StatusPublished
Author(s)Maharaj, Savi; Gunter, Elsa L
Title of seriesLecture Notes in Computer Science
Number in series859
Publication date31/12/1994
Publication date online30/09/1994
PublisherSpringer
Publisher URLhttp://link.springer.com/chapter/10.1007/3-540-58450-1_53#
Place of publicationBerlin Heidelberg
ISSN of series0302-9743
ISBN978-3-540-58450-6
Conference7th International Workshop on Higher Order Logic Theorem Proving and Its Applications
Conference locationValletta, Malta
Dates
Scroll back to the top