1: \begin{thebibliography}{10}
2:
3: \bibitem{Aiken99SetConstraintsIntro}
4: Alexander Aiken.
5: \newblock Introduction to set constraint-based program analysis.
6: \newblock {\em Science of Computer Programming}, 35:79--111, 1999.
7:
8: \bibitem{AikenETAL95DecidabilitySetConstraints}
9: Alexander Aiken, Dexter Kozen, and Ed~Wimmers.
10: \newblock Decidability of systems of set constraints with negative constraints.
11: \newblock {\em Information and Computation}, 122, 1995.
12:
13: \bibitem{AikenETAL94SoftTypingConditionalTypes}
14: Alexander Aiken, Edward~L. Wimmers, and T.~K. Lakshman.
15: \newblock Soft typing with conditional types.
16: \newblock In {\em Proc. 21st ACM POPL}, pages 163--173, New York, NY, 1994.
17:
18: \bibitem{AmadioCardelli93SubtypingRecursiveTypes}
19: Roberto~M. Amadio and Luca Cardelli.
20: \newblock Subtyping recursive types.
21: \newblock {\em Transactions on Programming Languages and Systems},
22: 15(4):575--631, 1993.
23:
24: \bibitem{Andersen94ProgramAnalysisSpecializationCProgrammingLanguage}
25: L.~O. Andersen.
26: \newblock {\em Program Analysis and Specialization of the C Programming
27: Language}.
28: \newblock PhD thesis, DIKU, University of Copenhagen, 1994.
29:
30: \bibitem{BoergerETAL97ClassicalDecisionProblem}
31: Egon B\"orger, Erich Gr\"aedel, and Yuri Gurevich.
32: \newblock {\em The Classical Decision Problem}.
33: \newblock Springer-Verlag, 1997.
34:
35: \bibitem{CharatonikPacholski94SetConstraintsProjections}
36: Witold Charatonik and Leszek Pacholski.
37: \newblock Set constraints with projections are in {NEXPTIME}.
38: \newblock In {\em Proc. 35th Annual Symposium on Foundations of Computer
39: Science (FOCS)}, pages 642--653, 1994.
40:
41: \bibitem{CharatonikPodelski97SetConstraintsIntersection}
42: Witold Charatonik and Andreas Podelski.
43: \newblock Set constraints with intersection.
44: \newblock In {\em Proc. 12th IEEE LICS}, pages 362--372, 1997.
45:
46: \bibitem{Comon91Disunification}
47: Hubert Comon.
48: \newblock Disunification: A survey.
49: \newblock In Jean-Louis Lassez and Gordon Plotnik, editors, {\em Computational
50: Logic: Essays in Honor of Alan Robinson}. The MIT Press, Cambridge, Mass.,
51: 1991.
52:
53: \bibitem{ComonDelor94EquationalFormulaeMembershipConstraints}
54: Hubert Comon and Catherine Delor.
55: \newblock Equational formulae with membership constraints.
56: \newblock {\em Information and Computation}, 112(2):167--216, 1994.
57:
58: \bibitem{ComonLescanne89EquationalProblemsDisunification}
59: Hubert Comon and Pierre Lescanne.
60: \newblock Equational problems and disunification.
61: \newblock {\em Journal of Symbolic Computation}, 7(3):371, 1989.
62:
63: \bibitem{Courcelle83FundamentalPropertiesInfiniteTrees}
64: Bruno Courcelle.
65: \newblock Fundamental properties of infinite trees.
66: \newblock {\em Theoretical Computer Science}, 25(2):95--169, March 1983.
67:
68: \bibitem{DaviesPfenning00IntersectionTypesComputationalEffects}
69: Rowan Davies and Frank Pfenning.
70: \newblock Intersection types and computational effects.
71: \newblock In {\em Proc.\ ICFP}, pages 198--208, 2000.
72:
73: \bibitem{FefermanVaught59FirstOrderPropertiesProductsAlgebraicSystems}
74: S.~Feferman and R.~L. Vaught.
75: \newblock The first order properties of products of algebraic systems.
76: \newblock {\em Fundamenta Mathematicae}, 47:57--103, 1959.
77:
78: \bibitem{FerranteRackoff79ComputationalComplexityLogicalTheories}
79: Jeanne Ferrante and Charles~W. Rackoff.
80: \newblock {\em The Computational Complexity of Logical Theories}, volume 718 of
81: {\em Lecture Notes in Mathematics}.
82: \newblock Springer-Verlag, 1979.
83:
84: \bibitem{FreemanPfenning91RefinementML}
85: Tim Freeman and Frank Pfenning.
86: \newblock Refinement types for {ML}.
87: \newblock In {\em Proc. ACM PLDI}, 1991.
88:
89: \bibitem{Frey02SubtypeInequalitiesPolynomialSpace}
90: Alexandre Frey.
91: \newblock Satisfying subtype inequalities in polynomial space.
92: \newblock {\em Theoretical Computer Science}, 277:105--117, 2002.
93:
94: \bibitem{GurevichHarrington82TreesAutomataGames}
95: Yuri Gurevich and Leo Harrington.
96: \newblock Trees, automata, and games.
97: \newblock In {\em Proceedings of the fourteenth annual ACM symposium on Theory
98: of computing}, pages 60--65, 1982.
99:
100: \bibitem{HeintzeTardieu01UltraFastAliasAnalysis}
101: Nevin Heintze and Olivier Tardieu.
102: \newblock Ultra-fast aliasing analysis using {CLA}: A million lines of {C} code
103: in a second.
104: \newblock In {\em Proc. ACM PLDI}, 2001.
105:
106: \bibitem{HengleinRehof97ComplexitySubtypeEntailmentSimpleTypes}
107: Fritz Henglein and Jakob Rehof.
108: \newblock The complexity of subtype entailment for simple types.
109: \newblock In {\em Proc. 12th IEEE LICS}, pages 352--361, 1997.
110:
111: \bibitem{HenkinETAL71CylindricAlgebrasPartI}
112: L.~Henkin, J.~D. Monk, and A.~Tarski.
113: \newblock {\em Cylindric Algebras, Part I}.
114: \newblock North Holland, 1971.
115:
116: \bibitem{Hodges93ModelTheory}
117: Wilfrid Hodges.
118: \newblock {\em Model Theory}, volume~42 of {\em Encyclopedia of Mathematics and
119: its Applications}.
120: \newblock Cambridge University Press, 1993.
121:
122: \bibitem{JimPalsberg99TypeInferenceSystemsRecursiveTypesSubtyping}
123: Trevor Jim and Jens Palsberg.
124: \newblock Type inference in systems of recursive types with subtyping.
125: \newblock \url{http://www.cs.purdue.edu/homes/palsberg/}, 1999.
126:
127: \bibitem{KerberKohlhase94MechanizationPartialFunctions}
128: Manfred Kerber and Michael Kohlhase.
129: \newblock A mechanization of strong {K}leene logic for partial functions.
130: \newblock In Alan Bundy, editor, {\em Proc. 12th CADE}, pages 371--385, Nancy,
131: France, 1994. Springer Verlag, Berlin, Germany.
132: \newblock LNAI 814.
133:
134: \bibitem{KlarlundETAL00MONA}
135: Nils Klarlund, Anders M{\o}ller, and Michael~I. Schwartzbach.
136: \newblock {MONA} implementation secrets.
137: \newblock In {\em Proc. 5th International Conference on Implementation and
138: Application of Automata}. Lecture Notes in Computer Science, 2000.
139:
140: \bibitem{Kleene52IntroductionMetamathematics}
141: Stephen~Cole Kleene.
142: \newblock {\em Introduction to Metamathematics}.
143: \newblock D. Van Nostrand Company, Inc., Princeton, New Jersey, 1952.
144: \newblock fifth reprint, 1967.
145:
146: \bibitem{Kozen80ComplexityBooleanAlgebras}
147: Dexter Kozen.
148: \newblock Complexity of boolean algebras.
149: \newblock {\em Theoretical Computer Science}, 10:221--247, 1980.
150:
151: \bibitem{KozenETAL95EfficientRecursiveSubtyping}
152: Dexter Kozen, Jens Palsberg, and Michael~I. Schwartzbach.
153: \newblock Efficient recursive subtyping.
154: \newblock {\em Mathematical Structures in Computer Science}, 5(1):113--125,
155: 1995.
156:
157: \bibitem{Lloyd87FoundationsLogicProgramming}
158: John~W. Lloyd.
159: \newblock {\em Foundations of Logic Programming}.
160: \newblock Springer-Verlag, 2nd edition, 1987.
161:
162: \bibitem{Maher88CompleteAxiomatizationsAlgebrasTrees}
163: Michael~J. Maher.
164: \newblock Complete axiomatizations of the algebras of the finite, rational, and
165: infinite trees.
166: \newblock {\em Proc. 3rd IEEE LICS}, 1988.
167:
168: \bibitem{Malcev71MetamathematicsAlgebraicSystems}
169: Anatolii~Ivanovic Mal'cev.
170: \newblock {\em The Metamathematics of Algebraic Systems}, volume~66 of {\em
171: Studies in Logic and The Foundations of Mathematics}.
172: \newblock North Holland, 1971.
173:
174: \bibitem{MartinNipkow89BooleanUnification}
175: Ursula Martin and Tobias Nipkow.
176: \newblock Boolean unification: The story so far.
177: \newblock {\em Journal of Symbolic Computation}, 7(3):275--293, 1989.
178:
179: \bibitem{McCarthyPainter67CorrectnessCompilerArithmeticExpressions}
180: John McCarthy and James Painter.
181: \newblock Correctness of a compiler for arithmetic expressions.
182: \newblock In {\em Proceedings of Symposia in Applied Mathematics}. American
183: Mathematical Society, 1967.
184:
185: \bibitem{Mitchell91TypeInferenceSimpleTypes}
186: John~C. Mitchell.
187: \newblock Type inference with simple types.
188: \newblock {\em Journal of Functional Programming}, 1(3):245--285, 1991.
189:
190: \bibitem{Mostowski52DirectProductsTheories}
191: Andrzej Mostowski.
192: \newblock On direct products of theories.
193: \newblock {\em Journal of Symbolic Logic}, 17(1):1--31, March 1952.
194:
195: \bibitem{MuellerNiehren00OrderingConstraintsFeatureTreesMSOL}
196: Martin Mueller and Joachim Niehren.
197: \newblock Ordering constraints over feature trees expressed in second-order
198: monadic logic.
199: \newblock {\em Information and Computation}, 159(1/2):22--58, 2000.
200:
201: \bibitem{MuellerETAL01OrderingConstraintsFeatureTrees}
202: Martin Mueller, Joachim Niehren, and Ralf Treinen.
203: \newblock The first-order theory of ordering constraints over feature trees.
204: \newblock {\em Discrete Mathematics and Theoretical Computer Science},
205: 4(2):193--234, September 2001.
206:
207: \bibitem{NelsonOppen80DecisionProceduresCongruenceClosure}
208: Greg Nelson and Derek~C. Oppen.
209: \newblock Fast decision procedures based on congruence closure.
210: \newblock {\em Journal of the ACM (JACM)}, 27(2):356--364, 1980.
211:
212: \bibitem{Oppen80ReasoningRecursivelyDefinedDataStructures}
213: Derek~C. Oppen.
214: \newblock Reasoning about recursively defined data structures.
215: \newblock {\em Journal of the ACM}, 27(3), 1980.
216:
217: \bibitem{Pfenning91UnificationCalculusConstructions}
218: Frank Pfenning.
219: \newblock Unification and anti-unification in the calculus of constructions.
220: \newblock In {\em Proc. 6th IEEE LICS}, pages 74--85, 1991.
221:
222: \bibitem{Pottier01SimplifyingSubtypingConstraints}
223: Francois Pottier.
224: \newblock Simplifying subtyping constraints: {A} theory.
225: \newblock {\em Information and Computation}, 170(2):153--183, November 2001.
226:
227: \bibitem{Rehof98ComplexitySimpleSubtypingSystems}
228: Jakob Rehof.
229: \newblock {\em The Complexity of Simple Subtyping Systems}.
230: \newblock PhD thesis, Computer Science Department, Univ. of Copenhagen (DIKU),
231: April 1998.
232:
233: \bibitem{RybinaVoronkov01DecisionProcedureTermAlgebrasQueues}
234: Tatiana Rybina and Andrei Voronkov.
235: \newblock A decision procedure for term algebras with queues.
236: \newblock {\em ACM Transactions on Computational Logic (TOCL)}, 2(2):155--181,
237: 2001.
238:
239: \bibitem{SagivETAL02Parametric}
240: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
241: \newblock Parametric shape analysis via 3-valued logic.
242: \newblock {\em ACM TOPLAS}, 24(3):217--298, 2002.
243:
244: \bibitem{Siekmann89UnificationTheory}
245: J\"org~H. Siekmann.
246: \newblock Unification theory.
247: \newblock {\em Journal of Symbolic Computation}, 7(3):207--274, 1989.
248:
249: \bibitem{Skolem19Untersuchungen}
250: Thoralf Skolem.
251: \newblock Untersuchungen \"uber die {A}xiome des {K}lassenkalk\"uls and \"uber
252: ``{P}roduktations- und {S}ummationsprobleme'', welche gewisse {K}lassen von
253: {A}ussagen betreffen.
254: \newblock Skrifter utgit av {V}idnskapsselskapet i {K}ristiania, I. klasse, no.
255: 3, {O}slo, 1919.
256:
257: \bibitem{Steensgaard96PointsAnalysisAlmostLinearTime}
258: Bjarne Steensgaard.
259: \newblock Points-to analysis in almost linear time.
260: \newblock In {\em Proc. 23rd ACM POPL}, St. Petersburg Beach, FL, January 1996.
261:
262: \bibitem{SuETAL02FirstOrderTheorySubtypingConstraints}
263: Zhendong Su, Alexander Aiken, Joachim Niehren, Tim Priesnitz, and Ralf Treinen.
264: \newblock First-order theory of subtyping constraints.
265: \newblock In {\em Proc. 29th ACM POPL}, 2002.
266:
267: \bibitem{Sudan02QuantifierEliminationBooleanAlgebrasTrivial}
268: Madhu Sudan.
269: \newblock Quantifier elimination for boolean algebras is trivial.
270: \newblock Personal Communication, MIT LCS Elevator, 9 October 2002.
271:
272: \bibitem{Tarski49ArithmeticalClassesTypesAlgebraicallyClosed}
273: Alfred Tarski.
274: \newblock Arithmetical classes and types of algebraically closed and
275: real-closed fields.
276: \newblock {\em Bull.\ Amer.\ Math.\ Soc.}, 55, 64, 1192, 1949.
277:
278: \bibitem{Tarski49ArithmeticalClassesTypesBooleanAlgebras}
279: Alfred Tarski.
280: \newblock Arithmetical classes and types of boolean algebras.
281: \newblock {\em Bull.\ Amer.\ Math.\ Soc.}, 55, 64, 1192, 1949.
282:
283: \bibitem{Thomas90AutomataInfiniteObjects}
284: Wolfgang Thomas.
285: \newblock Automata on infinite objects.
286: \newblock In {\em Handbook of Theoretical Computer Science, Volume B}, pages
287: 133--191. Elsevier and The MIT Press, 1990.
288:
289: \bibitem{Thomas97LanguagesAutomataLogic}
290: Wolfgang Thomas.
291: \newblock Languages, automata, and logic.
292: \newblock In {\em Handbook of Formal Languages Vol.3: Beyond Words}.
293: Springer-Verlag, 1997.
294:
295: \bibitem{Tiuryn92SubtypeInequalities}
296: Jerzy Tiuryn.
297: \newblock Subtype inequalities.
298: \newblock In {\em Proc. 7th IEEE LICS}, 1992.
299:
300: \bibitem{Venkataraman87DecidabilityExistentialTermAlgebras}
301: K.~N. Venkataraman.
302: \newblock Decidability of the purely existential fragment of the theory of term
303: algebras.
304: \newblock {\em Journal of the ACM (JACM)}, 34(2):492--510, 1987.
305:
306: \bibitem{Walukiewicz96MonadicSecondOrderLogicTreeLikeStructures}
307: Igor Walukiewicz.
308: \newblock Monadic second-order logic on tree-like structures.
309: \newblock In {\em STACS'96}, volume 1046 of {\em Lecture Notes in Computer
310: Science}, 1996.
311:
312: \bibitem{Walukiewicz02MonadicSecondOrderLogicTreeLikeStructures}
313: Igor Walukiewicz.
314: \newblock Monadic second-order logic on tree-like structures.
315: \newblock {\em Theoretical Computer Science}, 275(1--2):311--346, March 2002.
316:
317: \end{thebibliography}
318: