Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Logical Aspects of Set Constraints
Authors: Kozen, Dexter
Keywords: computer science
technical report
Issue Date: May-1994
Publisher: Cornell University
Abstract: Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational axiomatization of the algebra of set constraints. Models of these axioms are called termset algebras. They are related to the Boolean algebras with operators of Jonsson and Tarski. We also define a family of combinatorial models called topological term automata, which are essentially the term automata studied by Kozen, Palsberg, and Schwartzbach endowed with a topology such that all relevant operations are continuous. These models are similar to Kripke frames for modal or dynamic logic. We establish a Stone duality between termset algebras and topological term automata, and use time to derive a completeness theorem for a related multidimensional modal logic. Finally, we prove a small model property by filtration, and argue that this result contains the essence of several algorithms appearing in the literature on set constraints.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
94-1421.pdf1.06 MBAdobe PDFView/Open
94-1421.ps290.67 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us