Strategies for solving constraints in program analysis

Jurriaan Hage, Bastiaan Heeren

Research output: Book/ReportOther report


Type and effect systems are typically specified as a system of
logical deduction rules, which specify what are valid types and
effects in a program. Converting such a system into an algorithm
is typically a lot of error-prone work, and usually results in an
implementation that performs its task inflexibly, leaving no room
to modify the solving strategy, without changing the algorithm.
In this paper we take a constraint-based approach to declaratively specify a type system. Our contribution is to enrich the type
rules by the use of a fixed set of combinators. By choosing a semantics for these combinators, we obtain particular orderings of
the constraints, which can then be fed into a constraint solver. Thus they bridge the gap between the declarative specification and a deterministic implementation of type systems. The main advantages are that the issue of the order in which constraints should be solved is factored out of the solver, making the solver simpler and more amenable to reuse; the user of the solver can flexibly choose a particular solving strategy; and it makes the implementation of type and effect systems a much easier and less error-prone task. Our combinators have been implemented into a fully functional compiler.
Original languageEnglish
PublisherDepartment of Information and Computing Sciences, Utrecht University
Number of pages10
Publication statusPublished - 2006

Publication series

NameTechnical Report Series
ISSN (Print)0924-3275


Dive into the research topics of 'Strategies for solving constraints in program analysis'. Together they form a unique fingerprint.

Cite this