Skip to main content
SpringerLink
Log in

Backward Type Inference Generalises Type Checking

  • Conference paper
  • First Online:
Static Analysis (SAS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2477))

Included in the following conference series:

Abstract

This paper presents a backward type analysis for logic programs. Given type signatures for a collection of selected predicates such as builtin or library predicates, the analysis infers type signatures for other predicates such that the execution of any query satisfying the inferred type signatures will not violate the type signatures for the selected predicates. Thus, the backward type analysis generalises type checking in which the programmer manually specifies type signatures for all predicates that are checked for consistency by a type checker.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Barbuti and R. Giacobazzi. A bottom-up polymorphic type inference in logic programming. Science of Computer Programming, 19(3):133–181, 1992.

    Article  MathSciNet  Google Scholar 

  2. M. Codish and B. Demoen. Deriving polymorphic type dependencies for logic programs using multiple incarnations of Prop. In Proceedings of International Static Analysis Symposium, pages 281–297. Springer-Verlag, 1994.

    Google Scholar 

  3. M. Codish and V. Lagoon. Type dependencies for logic programs using ACI-unification. Theoretical Computer Science, 238:131–159, 2000.

    Article  MATH  MathSciNet  Google Scholar 

  4. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Type analysis of Prolog using type graphs. Journal of Logic Programming, 22(3):179–208, 1995.

    Article  MATH  Google Scholar 

  5. A. Cortesi, G. Filé, and W. Winsborough. Optimal groundness analysis using propositional logic. Journal of Logic Programming, 27(2): 137–168, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. P. Cousot and R. Cousot. Abstract interpretation: a unified framework for static analysis of programs by construction or approximation of fixpoints. In Proceedings of Principles of Programming Languages, pages 238–252. The ACM Press, 1977.

    Google Scholar 

  7. P.W. Dart and J. Zobel. A regular type language for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 157–189. The MIT Press, 1992.

    Google Scholar 

  8. J.P. Gallagher and D.A. de Waal. Fast and precise regular approximations of logic programs. In Proceedings of International Conference on Logic Programming, pages 599–613. The MIT Press, 1994.

    Google Scholar 

  9. N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. In Proceedings of Principles of Programming Languages, pages 197–209. The ACM Press, 1990.

    Google Scholar 

  10. N. Heintze and J. Jaffar. Semantic types for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 141–155. The MIT Press, 1992.

    Google Scholar 

  11. K. Horiuchi and T. Kanamori. Polymorphic type inference in Prolog by abstract interpretation. In Proceedings of Conference on Logic Programming, pages 195–214. Springer, 1988.

    Google Scholar 

  12. G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming, 13(1–4):205–258, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. T. Kanamori and K. Horiuchi. Type inference in Prolog and its application. In Proceedings of International Joint Conference on Artificial Intelligence, pages 704–707. Morgan Kaufmann, 1985.

    Google Scholar 

  14. T. Kanamori and T. Kawamura. Abstract interpretation based on OLDT resolution. Journal of Logic Programming, 15(1 & 2): 1–30, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  15. A. King and L. Lu. A backward analysis for constraint logic programs. Theory and Practice of Logic Programming, 2(4&5):517–547, 2002.

    Article  MATH  MathSciNet  Google Scholar 

  16. J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.

    Google Scholar 

  17. L. Lu. A polymorphic type analysis in logic programs by abstract interpretation. Journal of Logic Programming, 36(1):1–54, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  18. L. Lu. A precise type analysis of logic programs. In Proceedings of International Conference on Principles and Practice of Declarative Programming, pages 214–225. The ACM Press, 2000.

    Google Scholar 

  19. K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Letters on Programming Languages and Systems, 2(1–4): 181–196, 1993.

    Article  Google Scholar 

  20. P. Mishra. Towards a theory of types in Prolog. In Proceedings of the IEEE International Symposium on Logic Programming, pages 289–298. The IEEE Computer Society Press, 1984.

    Google Scholar 

  21. D. Pedreschi and S. Ruggieri. Weakest preconditions for pure Prolog programs. Information Processing Letters, 67(3):145–150, 1998.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oakland University, MI, 48309, USA

    Lunjin Lu

  2. University of Kent at Canterbury, CT2 7NF, UK

    Andy King

Authors
  1. Lunjin Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science Facultad de Informática, Technical University of Madrid, Campus de Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Manuel V. Hermenegildo  & Germán Puebla  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lu, L., King, A. (2002). Backward Type Inference Generalises Type Checking. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-45789-5_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44235-6

  • Online ISBN: 978-3-540-45789-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation