@Inproceedings{Gly-Stu-Sul-Son:pado01,
  author   = {Kevin Glynn and Peter J. Stuckey and Martin Sulzmann and
                Harald S{\o}ndergaard},
  title    = {Boolean Constraints for Binding-Time Analysis},
  editor   = {O. Danvy and A. Filinsky},
  booktitle= {Programs as Data Objects: Proceedings of the Second Symposium},
  series   = {Lecture Notes in Computer Science},
  volume   = {2053},
  pages    = {39--63},
  publisher= {Springer},
  year     = {2001},
  abstract = {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.
             },
}