Defining soft sortedness by abstract interpretation

  • Jian Chen
  • John Staples
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


Sorted languages can improve the expressiveness and efficiency of reasoning. A conventional sorted language typically includes well-sortedness rules amongst the rules for well-formedness. A major disadvantage of this approach is that many intuitively meaningful expressions are ill-sorted and hence not part of the language.

To overcome this limitation, soft sorting regards as well-formed, all first-order expressions of the corresponding unsorted language, and lets the semantics be the basis for defining the significance of the sort syntax. In this paper we show how soft sortedness can be defined by abstract interpretations which characterise semantic properties of softly sorted expressions.


Logic Program Abstract Interpretation Predicate Symbol Domain Universe Soft Typing 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramsky, S. and Hankin, C. (eds.), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.Google Scholar
  2. 2.
    Cartwright, R. and M. Fagan, “Soft Typing”, in Proceedings of the ACM SIG-PLAN'91 Conference on Programming Language Design and Implementation, pages 278–292, 1991.Google Scholar
  3. 3.
    Chen, J., “Soft Sorting: Integrating Static and Dynamic Sort Checking”, PhD thesis, Department of Computer Science, The University of Queensland, Australia, 1992.Google Scholar
  4. 4.
    Chen, J. and J. Staples, “Soft Sorting in Logic Programming”, in Proceedings of ALPUK'92, Springer-Verlag, pages 79–96, 1992.Google Scholar
  5. 5.
    Cohn, A. G., “A More Expressive Formulation of Many Sorted Logic”, JAR 3(1987) 113–200.Google Scholar
  6. 6.
    Comon, H., “Disunification: A Survey”, in Computational Logic: Essays in Honor of Alan Robinson, Lassez, J.-L. and Plotkin, G. (eds.), The MIT Press, 1991, 322–359.Google Scholar
  7. 7.
    Enderton, H. B., A Mathematical Introduction to Logic, Academic Press, 1972.Google Scholar
  8. 8.
    Henglein, F., “Dynamic Typing”, in Proceedings of the 4th European Symposium on Programming (ESOP '92), pages 233–253, LNCS 582, Springer-Verlag, 1992.Google Scholar
  9. 9.
    Hill, P. M. and R. W. Topor, “A Semantics for Typed Logic Programs”, in Pfenning, F., (ed.), Types in Logic Programming, The MIT Press, pages 1–62, 1992.Google Scholar
  10. 10.
    Kifer, M. and J. Wu, “A First-Order Theory of Typed and Polymorphism in Logic Programming”, in Proceedings of LICS '91, pages 310–321, 1991.Google Scholar
  11. 11.
    Lassez, J.-L., M. J. Maher and K. Marriott, “Unification Revisited”, in Foundations of Deductive Databases and Logic Programming, Minker, J. (ed.), Morgan Kaufmann Publishers, pages 587–625, 1988.Google Scholar
  12. 12.
    Lloyd, J. W., Foundations of Logic Programming, Springer-Verlag, 1987.Google Scholar
  13. 13.
    Mycroft, A. and R. A. O'Keefe, “A Polymorphic Type System for Prolog”, Artificial Intelligence 23, 295–307, 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Jian Chen
    • 1
  • John Staples
    • 1
  1. 1.Software Verification Research CentreThe University of QueenslandBrisbaneAustralia

Personalised recommendations