Abstract interpretation for type checking

  • G. Filè
  • P. Sottero
Session: Abstract Interpretation
Part of the Lecture Notes in Computer Science book series (LNCS, volume 528)


The typed logic languages are more expressive than the usual untyped ones, but run-time type-checking is in general quite costly. Compile-time type checking is a classical application of the abstract interpretation paradigm. We describe a general abstract interpretation framework and inside it we develop two new methods for the compile-time type-checking of typed logic programs. The first method applies to a restricted class of programs (those that are type-preserving and use a finite number of types) and it detects the programs that need no type-checking at all. The second one applies to any program, but, in general, it only avoids part of the run-time type-checking.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [APe90]
    K.Apt & D.Pedreschi; Studies in pure Prolog: termination. Proc. Symp. on Computational Logic, Lec. Notes in AI, n.1, Springer Verlag, 1990.Google Scholar
  2. [Bak57]
    J.Bakus et al.; The FORTRAN automatic coding system. Western Joint Computer Conf. (1957), 188–198.Google Scholar
  3. [BAK89]
    R.N.Bol, K.A.Apt, J.W.Klop; An analysis of loop checking mechanisms for logic programs. CWI, R. CS-R8942, 1989.Google Scholar
  4. [BCF90]
    A.Bossi, N.Cocco & M.Fabris; Proving termination of logic programs by exploiting term properties. Dep. of Math., Univ. of Padova, R.21, 1990. Accepted to the TAPSOFT Conf., Brighton, 1991.Google Scholar
  5. [Bez89]
    M.Bezem; Characterizing termination of logic programs with level mappings. Proc. North American conf. on Logic Programming, Cleveland, eds. L.Lusk & R.Overbeek, MIT Press, (1989), 69–80.Google Scholar
  6. [Bru88]
    M.Bruijhooghe; A practical framework for the abstract interpretation of logic programs. To appear in the J. of Logic Programming.Google Scholar
  7. [CFi 91]
    A.Cortesi & G.Filè; Abstract Interpretation: an abstract domain for groundness, sharing, freeness and compoundness analysis. Dep. of Math., University of Padova, R.4-1991; also to appear in the Proc. of the ACM SIGPLAN Symposium on partial evaluation and semantics based program manipulation, New Haven, 1991.Google Scholar
  8. [CoF91]
    P.Codognet & G.Filè; Coomputations, abstractions and constraints. In preparation.Google Scholar
  9. [Han89]
    M.Hanus; Horn clause programs with polymorphic types: semantics and resolution. Proc. of TAPSOFT 89, LNCS 352, 225–240.Google Scholar
  10. [KKa90]
    T.Kanamori & T.Kawamura; Abstract interpretation based on OLDT-resolution. ICOT TR, 1990.Google Scholar
  11. [Llo87]
    J.Lloyd; Foundations of logic programming. Springer Verlag, 2nd edition, 1987.Google Scholar
  12. [Mil78]
    R. Milner; A theory of type polymorphism in programming. J.Comput. System Sci. 17, (1978), 348–375.Google Scholar
  13. [MO'K84]
    A. Mycroft & R. O'Keefe; A polymorphic type system for Prolog. Artificial intelligence 23, (1984), 295–307.Google Scholar
  14. [MSo89]
    K. Merriot & H. Sondergaard; A tutorial on abstract interpretation of logic program. Tutorial of the North American conf. on Logic Programming, Cleveland, 1989.Google Scholar
  15. [Nau65]
    P. Naur; Checking of operand types in Algol compilers. BIT 5, (1965), 151–163.Google Scholar
  16. [TSa86]
    H. Tamaki & T. Sato; OLD resolution with tabulation. Proc. of the 3rd Conf. on Logic programming, London, LNCS 225, (1986), 84–98.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • G. Filè
    • 1
  • P. Sottero
    • 1
  1. 1.Dep. of Pure and Applied MathematicsUniversity of PadovaItaly

Personalised recommendations