Inferring program specifications in polynomial-time

  • Robert Givan
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


We consider the problem of automatically inferring properties of programs. Our approach is to explore the application of familiar type inference principles to a “type system∝ sufficiently expressive that the typing problem is effectively the checking of program specifications. We use familiar syntax-directed type inference rules to give a polynomialtime procedure for inferring type theorems in this rich type system. We discuss examples of simple functional programs and the specification information this procedure automatically infers. The enriched notion of type allows the definition of any recursively enumerable set as a type, and includes argument-dependent output types for functions. The inference procedure is capable for example of automatically inferring that an insertion sort program always returns a sorted permutation of its input.


Functional Programming Type Inference Verification Induction 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Aiken and E. Wimmers. Soft typing with conditional types. In ACM Symposium on Principles of Programming Languges, pages 163–173, 1994.Google Scholar
  2. 2.
    Alexander Aiken and Edward Wimmers. Type inference with set constraints. Research Report 8956, IBM, 1992.Google Scholar
  3. 3.
    J. A. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10:19–35, 1980.CrossRefGoogle Scholar
  4. 4.
    R. L. Constable et. al. Implementing Mathematics with the Nuprl Development system. Prentice-Hall, 1986.Google Scholar
  5. 5.
    Robert Givan. Automatically Inferring Properties of Computer Programs. PhD thesis, Massachusetts Institute of Technology, 1996. Scholar
  6. 6.
    P. Jouvelot and D. Gifford. Algebraic reconstruction of types and effects. In Proceedings of ACM Conference on Principles of Programming Languages, 1991.Google Scholar
  7. 7.
    D. McAllester and K. Arkoudas. Walther recursion. Submitted to CADE-13, available at, 1996.Google Scholar
  8. 8.
    D. McAllester and R. Givan. Taxonomic syntax for first order inference. JACM, 40(2):246–283, April 1993. internet file Scholar
  9. 9.
    J. McCarthy. A basis for a math. theory of computation. P. Braffort & D. Hirschberg, eds., Computer Programing & Formal Systems. North-Holland, 1967.Google Scholar
  10. 10.
    Robin Milner. Type polymorphism in programming. JCSS, 17:348–375, 1978.Google Scholar
  11. 11.
    John C. Mitchell. A type inference appproach to reduction properties and semantics of polymorphic expressions. In Proceedings 1986 ACM Symposium on Lisp and Functional Programming, pages 308–319, 1986.Google Scholar
  12. 12.
    P. Mishra and U. S. Reddy. Declaration-free type checking. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 7–21. ACM, 1985.Google Scholar
  13. 13.
    John C. Reynolds. Towards a theory of type structure. In Proceedings Colloque sur la Programmation. Springer-Verlag, 1974.Google Scholar
  14. 14.
    J.W. Thatcher. Tree automata: an informal survey. In A. V. Aho, editor, Currents in Theory of Computation, pages 143–172. Prentice-Hall, 1973.Google Scholar
  15. 15.
    W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B, Formal Methods and Semantics, pp. 133–164. MIT Press, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Robert Givan
    • 1
  1. 1.Massachusetts Institute of TechnologyCambridgeUSA

Personalised recommendations