TY - GEN
T1 - HOL-ML
AU - Vanlnwegen, Myra
AU - Gunter, Elsa
PY - 1994
Y1 - 1994
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84867755437&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84867755437&partnerID=8YFLogxK
U2 - 10.1007/3-540-57826-9_125
DO - 10.1007/3-540-57826-9_125
M3 - Conference contribution
AN - SCOPUS:84867755437
SN - 9783540578260
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 61
EP - 74
BT - Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
A2 - Joyce, Jeffrey J.
A2 - Seger, Carl-Johan H.
PB - Springer
T2 - 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993
Y2 - 11 August 1993 through 13 August 1993
ER -