@inproceedings{6c4eb1f8a2f64bf8b64bc9a7858f310a,
title = "An abstract interpretation for ML equality kinds",
abstract = "The definition of Standard ML provides a form of generic equality which is inferred for certain types, called equality types, on which it is possible to define a computable equality relation. However~ the standard definition is incomplete in the sense that there are interesting and useful types which are not inferred to be equality types but which nevertheless have a computable equality relation. In this paper, a refinement of the Standard ML system of equality types is introduced and is proven sound and complete with respect to the existence of a computable equality. The technique used here is based on an abstract interpretation of ML operators as monotone functions over a three point lattice. It is shown how the equality relation can be defined (as an ML program) from the definition of a type with our equality property. Finally, a sound, efficient algorithm for inferring the equality property which corrects the limitations of the standard definition in all cases of practical interest is demonstrated.",
author = "Gunter, {Carl A.} and Gunter, {Elsa L.} and MacQueen, {David B.}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1991.; 1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 ; Conference date: 24-09-1991 Through 27-09-1991",
year = "1991",
doi = "10.1007/3-540-54415-1_43",
language = "English (US)",
isbn = "9783540544159",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "112--130",
editor = "Meyer, {Albert R.} and Takayasu Ito",
booktitle = "Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings",
address = "Germany",
}