An abstract interpretation for ML equality kinds

Carl A. Gunter, Elsa L. Gunter, David B. MacQueen

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

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.

Original languageEnglish (US)
Title of host publicationTheoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings
EditorsAlbert R. Meyer, Takayasu Ito
PublisherSpringer-Verlag Berlin Heidelberg
Pages112-130
Number of pages19
ISBN (Print)9783540544159
DOIs
StatePublished - 1991
Externally publishedYes
Event1st International Conference on Theoretical Aspects of Computer Software, TACS 1991 - Sendai, Japan
Duration: Sep 24 1991Sep 27 1991

Publication series

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

Other

Other1st International Conference on Theoretical Aspects of Computer Software, TACS 1991
CountryJapan
CitySendai
Period9/24/919/27/91

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'An abstract interpretation for ML equality kinds'. Together they form a unique fingerprint.

  • Cite this

    Gunter, C. A., Gunter, E. L., & MacQueen, D. B. (1991). An abstract interpretation for ML equality kinds. In A. R. Meyer, & T. Ito (Eds.), Theoretical Aspects of Computer Software - International Conference TACS 1991, Proceedings (pp. 112-130). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 526 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/3-540-54415-1_43