BRICS · Contents · Programme · References

Set Constraints

A BRICS Mini-Course
August 14 and 15, 1996

Lectures by
Dexter Kozen
Joseph Newton Pew, Professor of Computer Science
Cornell University, Ithaca, NY, USA

Course Contents

Set constraints are equations involving expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this minicourse we will give an introduction to the theory and applications of set constraints.

The course will consist of six hours divided into three two-hour sessions. The first session will cover the basic definitions of set constraints, tree set automata and hypergraphs, closed hypergraphs, and regular solutions, and will cover basic applications in type theory and program analysis.

In the second session, we will discuss the complexity of set constraints and show a hierarchy of complexity results depending on the form of the language. We will also discuss more recent work on complexity of Tarskian set constraints, i.e. set constraints over non-Herbrand models, and constraint logic programming with set constraints.

Finally, in the last session we will go more deeply into the theory of set constraints. In particular we will discuss connections with other typing disciplines, including a duality between ``soft'' and ``hard'' typing, and give an introduction to the theory of rational spaces.

Programme

Wednesday August 14, 1996, 10:15-12:00 in Colloquium D4

Wednesday August 14, 1996, 14:15-16:00 in Colloquium D4

Thursday August 15, 1996, 10:15-12:00 in Colloquium D4

References

  1. A. Aiken, D. Kozen, M. Vardi, and E. Wimmers, The complexity of set constraints, in Proc. 1993 Conf. Computer Science Logic (CSL'93), E. Börger, Y. Gurevich, and K. Meinke, eds., vol. 832 of Lect. Notes in Comput. Sci., Eur. Assoc. Comput. Sci. Logic, Springer, September 1993, pp. 1-17.
  2. A. Aiken, D. Kozen, and E. Wimmers, Decidability of systems of set constraints with negative constraints, Infor. and Comput., 122 (1995), pp. 30-44.
  3. A. Aiken and B. Murphy, Implementing regular tree expressions, in Proc. 1991 Conf. Functional Programming Languages and Computer Architecture, August 1991, pp. 427-447.
  4. A. Aiken and B. Murphy, Static type inference in a dynamically typed language, in Proc. 18th Symp. Principles of Programming Languages, ACM, January 1991, pp. 279-290.
  5. A. Aiken and E. Wimmers, Solving systems of set constraints, in Proc. 7th Symp. Logic in Computer Science, IEEE, June 1992, pp. 329-340.
  6. L. Bachmair, H. Ganzinger, and U. Waldmann, Set constraints are the monadic class, in Proc. 8th Symp. Logic in Computer Science, IEEE, June 1993, pp. 75-83.
  7. J. A. Brzozowski and E. Leiss, On equations for regular languages, finite automata, and sequential networks, Theor. Comput. Sci., 10 (1980), pp. 19-35.
  8. W. Charatonik and L. Pacholski, Negative set constraints with equality, in Proc. 9th Symp. Logic in Computer Science, IEEE, July 1994, pp. 128-136.
  9. W. Charatonik and L. Pacholski, Set constraints with projections are in NEXPTIME, in Proc. 35th Symp. Foundations of Computer Science, IEEE, November 1994, pp. 642-653.
  10. A. Cheng and D. Kozen, A complete Gentzen-style axiomatization for set constraints, Tech. Rep. TR95-1518, Cornell University, May 1995. ICALP'96, to appear.
  11. A. Cheng and D. Kozen, Some notes on rational spaces, Tech. Rep. TR96-1576, Cornell University, March 1996.
  12. R. Gilleron, S. Tison, and M. Tommasi, Solving systems of set constraints using tree automata, in Proc. Symp. Theor. Aspects of Comput. Sci., vol. 665, Springer-Verlag Lect. Notes in Comput. Sci., February 1993, pp. 505-514.
  13. R. Gilleron, S. Tison, and M. Tommasi, Solving systems of set constraints with negated subset relationships, in Proc. 34th Symp. Foundations of Comput. Sci., IEEE, November 1993, pp. 372-380.
  14. R. Givan, D. Kozen, D. McAllester, and C. Witty, Tarskian set constraints. Manuscript. LICS'96, to appear., October 1994.
  15. N. Heintze, Set Based Program Analysis, PhD thesis, Carnegie Mellon University, 1993.
  16. N. Heintze and J. Jaffar, A decision procedure for a class of set constraints, in Proc. 5th Symp. Logic in Computer Science, IEEE, June 1990, pp. 42-51.
  17. N. Heintze and J. Jaffar, A finite presentation theorem for approximating logic programs, in Proc. 17th Symp. Principles of Programming Languages, ACM, January 1990, pp. 197-209.
  18. N. D. Jones and S. S. Muchnick, Flow analysis and optimization of LISP-like structures, in Proc. 6th Symp. Principles of Programming Languages, ACM, January 1979, pp. 244-256.
  19. D. Kozen, Logical aspects of set constraints, in Proc. 1993 Conf. Computer Science Logic (CSL'93), E. Börger, Y. Gurevich, and K. Meinke, eds., vol. 832 of Lect. Notes in Comput. Sci., Eur. Assoc. Comput. Sci. Logic, Springer, September 1993, pp. 175-188.
  20. D. Kozen, Set constraints and logic programming, Tech. Rep. 94-1467, Cornell University, November 1994.
  21. D. Kozen, Set constraints and logic programming (abstract), in Proc. First Conf. Constraints in Computational Logics (CCL'94), J.-P. Jouannaud, ed., vol. 845 of Lect. Notes in Comput. Sci., ESPRIT, Springer, September 1994, pp. 302-303.
  22. D. Kozen, Rational spaces and set constraints, in Proc. Sixth Int. Joint Conf. Theory and Practice of Software Develop. (TAPSOFT'95), P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, eds., vol. 915 of Lect. Notes in Comput. Sci., Springer, May 1995, pp. 42-61.
  23. D. Kozen, Set constraints and logic programming, Information and Computation, (1995). Accepted for publication.
  24. D. Kozen, Rational spaces and set constraints, Theoretical Computer Science A, 167 (1996). To appear.
  25. K. Marriott and M. Odersky, Systems of negative Boolean constraints, Tech. Rep. YALEU/DCS/RR-900, Computer Science Department, Yale University, April 1992.
  26. P. Mishra, Towards a theory of types in PROLOG, in Proc. 1st Symp. Logic Programming, IEEE, 1984, pp. 289-298.
  27. P. Mishra and U. Reddy, Declaration-free type checking, in Proc. 12th Symp. Principles of Programming Languages, ACM, 1985, pp. 7-21.
  28. J. C. Reynolds, Automatic computation of data set definitions, in Information Processing 68, North-Holland, 1969, pp. 456-461.
  29. K. Stefánsson, Systems of set constraints with negative constraints are NEXPTIME-complete, in Proc. 9th Symp. Logic in Computer Science, IEEE, June 1994, pp. 137-141.
  30. J. Young and P. O'Keefe, Experience with a type evaluator, in Partial Evaluation and Mixed Computation, D. Bjørner, A. P. Ershov, and N. D. Jones, eds., North-Holland, 1988, pp. 573-581.