Boolean Constraints for Binding-Time Analysis

  • Kevin Glynn
  • Peter J. Stuckey
  • Martin Sulzmann
  • Harald Søndergaard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)


To achieve acceptable accuracy, many program analyses for functional programs are “property polymorphic”. That is, they can infer different input-output relations for a function at separate applications of the function, in a manner similar to type inference for a polymorphic language. We extend a property polymorphic (or “polyvariant”) method for binding-time analysis, due to Dussart, Henglein, and Mossin, so that it applies to languages with ML-style type polymorphism. The extension is non-trivial and we have implemented it for Haskell. While we follow others in specifying the analysis as a non-standard type inference, we argue that it should be realised through a translation into the well-understood domain of Boolean constraints. The expressiveness offered by Boolean constraints opens the way for smooth extensions to sophisticated language features and it allows for more accurate analysis.


Deduction System Type Scheme Type Inference Principal Type Constraint Language 
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.
    M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. Principles of Programming Languages, pages 147–160. ACM Press, 1999.Google Scholar
  2. 2.
    T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming, 31(1):3–45, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    K. Brace, R. Rudell, and R. Bryant. Efficient implementation of a BDD package. In Proc. 27th ACM/IEEE Design Automation Conf., pages 40–45. IEEE Computer Society Press, 1990.Google Scholar
  4. 4.
    L. Damas and R. Milner. Principal type-schemes for functional programs. In Proc. Ninth ACM Symp. Principles of Programming Languages, pages 207–212. ACM Press, 1982.Google Scholar
  5. 5.
    F. Damiani. Non-Standard Type Inference for Functional Programs. PhD thesis, Universitá di Torino, February 1998.Google Scholar
  6. 6.
    W. Dowling and J. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267–284, 1984.CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In A. Mycroft, editor, Proc. Second Int. Symp. Static Analysis, volume 983 of LNCS, pages 118–135. Springer-Verlag, 1995.Google Scholar
  8. 8.
    M. Fähndrich and J. Rehof. Type-based flow analysis: From polymorphic subtyping to CFL reachability. In Proc. Twenty-Eighth ACM Symp. Principles of Programming Languages. ACM Press, 2001.Google Scholar
  9. 9.
    J. S. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In Proc. 1999 ACM SIGPLAN Conf. Programming Language Design and Implementation, (SIGPLAN Notices 34(5)), pages 192–203. ACM Press, 1999.Google Scholar
  10. 10.
    K. Glynn, P. J. Stuckey, M. Sulzmann, and H. Søndergaard. Boolean constraints for binding-time analysis. Technical Report TR2000/14, Dept. of Computer Science and Software Engineering, The University of Melbourne, 2000.Google Scholar
  11. 11.
    J. Gustavsson and J. Svenningsson. Constraint abstractions. Proc. Second Symp. Programs as Data Objects (PADO II), Aarhus, Denmark, May 2001.Google Scholar
  12. 12.
    N. Heintze and J. Riecke. The SLam calculus: Programming with secrecy and integrity. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 365–377. ACM Press, 1998.Google Scholar
  13. 13.
    F. Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253–289, 1993.CrossRefGoogle Scholar
  14. 14.
    F. Henglein and C. Mossin. Polymorphic binding-time analysis. In D. Sannella, editor, Proc. European Symp. Programming (ESOP 94), volume 788 of LNCS, pages 287–301. Springer-Verlag, 1994.Google Scholar
  15. 15.
    N. Kobayashi. Type-based useless variable elimination. In Proc. 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (SIGPLAN Notices 34(11)), pages 84–93. ACM Press, 2000.Google Scholar
  16. 16.
    T. Mogensen. Binding time analysis for polymorphically typed higher order languages. In J. Diaz and F. Orejas, editors, Proc. Int. Conf. Theory and Practice of Software Development, volume 352 of LNCS, pages 298–312. Springer-Verlag, 1989.Google Scholar
  17. 17.
    S. L. Peyton Jones and A. Santos. A transformation-based optimiser for Haskell. Science of Computer Programming, 32(1-3):3–47, 1998.zbMATHCrossRefGoogle Scholar
  18. 18.
    F. Pottier and S. Conchon. Information flow inference for free. In Proc. 5th Int. Conf. Functional Programming (ICFP’00), pages 46–57. ACM Press, 2000.Google Scholar
  19. 19.
    F. Prost. A static calculus of dependencies for the λ-cube. In Proc. 15th IEEE Ann. Symp. Logic in Computer Science (LICS’ 2000), pages 267–278. IEEE Computer Society Press, 2000.Google Scholar
  20. 20.
    A. Sabelfeld and D. Sands. A PER model of secure information flow in sequential programs. In S. Swierstra, editor, Proc. European Symp. Programming (ESOP 99), volume 1576 of LNCS, pages 40–58. Springer, 1999.Google Scholar
  21. 21.
    V. Saraswat, M. Rinard, and P. Panangaden. Semantic foundations of concurrent constraint programming. In Proc. Eighteenth ACM Symp. Principles of Programming Languages, pages 333–352. ACM Press, 1991.Google Scholar
  22. 22.
    P. Schachte. Efficient ROBDD operations for program analysis. Australian Computer Science Communications, 18(1):347–356, 1996.Google Scholar
  23. 23.
    Z. Shao. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC’97), Amsterdam, The Netherlands, June 1997.Google Scholar
  24. 24.
    D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In Proc. ACM SIGPLAN’ 96 Conf. Programming Language Design and Implementation (SIGPLAN Notices 31(5)), pages 181–192. ACM Press, 1996.Google Scholar
  25. 25.
    D. Volpano and G. Smith. A type-based approach to program security. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development (TAPSOFT’ 97), volume 1214 of LNCS, pages 607–621. Springer, 1997.CrossRefGoogle Scholar
  26. 26.
    M. Wand and L. Siveroni. Constraint systems for useless variable elimination. In Proc. 26th ACM Symp. Principles of Programming Languages, pages 291–302. ACM Press, 1999.Google Scholar
  27. 27.
    K. Wansbrough and S. L. Peyton Jones. Once upon a polymorphic type. In Proc. 26th ACM Symp. Principles of Programming Languages, pages 15–28. ACM Press, 1999.Google Scholar
  28. 28.
    K. Wansbrough and S. L. Peyton Jones. Simple usage polymorphism. In Third ACM SIGPLAN Workshop on Types in Compilation (TIC 2000), 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Kevin Glynn
    • 1
  • Peter J. Stuckey
    • 1
  • Martin Sulzmann
    • 1
  • Harald Søndergaard
    • 1
  1. 1.Department of Computer Science and Software EngineeringThe University of MelbourneVictoriaAustralia

Personalised recommendations