The undecidability of the semi-unification problem

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The undecidability of the semi-unification problem

Full text

Pdf (701 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the twenty-second annual ACM symposium on Theory of computing table of contents

Baltimore, Maryland, United States

Pages: 468 - 476

Year of Publication: 1990

ISBN:0-89791-361-2

Authors

A. J. Kfoury	Dept of Computer Science, Boston University
J. Tiuryn	Institute of Mathematics, University of Warsaw
P. Urzyczyn	Institute of Mathematics, University of Warsaw

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 22, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/100216.100279 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	[1] Cosmadakis, S.S. and Kanellakis, P.C., "Functional and inclusion dependencies: a graph theoretic approach", in Advances in Computing Research, Vol. 3, edited by Kanellakis and Preparata, JAI Press, 1986.
	2	S S Cosmadakis , P C Kanellakis, Equational theories and database constraints, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.273-284, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22176]
	3	[3] Dörre, J. and Rounds, W., "On subsumption and semiunification in feature algebras", manuscript, Oct 1989 (submitted for publication).
	4	[4] Feferman, S. el al, editors, Collected Works of Kurt Gödel, Oxford Univ Press, 1986.
	5	Fritz Henglein, Type inference and semi-unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.184-197, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62701]
	6	[6] Hooper, P.K., "The undecidability of the Turing machine immortality problem", Ph.D. Thesis, Computation Laboratory Report BL-38, Harvard University, June 1965.
	7	P. C. Kanellakis , J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-115, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75286]
	8	Deepak Kapur , David R. Musser , Paliath Narendran , Jonathan Stillman, Semi-Unification, Proceedings of the Eighth Conference on Foundations of Software Technology and Theoretical Computer Science, p.435-454, December 21-23, 1988
	9	[9] Kfoury, A.J. and Tiuryn, J., "Type reconstruction in finite-rank fragments of the second-order ¿-calculus", Boston Univ Technical Report, No. 89-010, Oct. 1989 (to appear in Proc. of LICS 1990).
	10	A. Kfoury , J. Tiuryn , P. Urzyczyn, Computational consequences and partial solutions of a generalized unification problem, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.98-105, June 1989, Pacific Grove, California, United States
	11	[11] Kfoury, A.J., Tiuryn, J. and Urzyczyn, P., "An Analysis of ML typability", Boston Univ Technical Report, No. 89-009, Oct. 1989 (submitted for publication).
	12	Hans Leiß, On Type Inference for Object-Oriented Programming Languages, Proceedings of the 1st Workshop on Computer Science Logic, p.151-172, October 12-16, 1987
	13	[13] Leiss, H., "Decidability of semi-unification in two variables", Technical Report INF 2-ASE-9-89, Siemens, Munchen, July 1989.
	14	John C. Mitchell, The implication problem for functional and inclusion dependencies, Information and Control, v.56 n.3, p.154-173, March 1983 [doi>10.1016/S0019-9958(83)80002-3]
	15	Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
	16	[16] Parikh, R.J., "Some results on the length of proofs", Trans. Amer. Math. Soc., 177, pp. 29- 36, March 1973.
	17	[17] Pudlák, P., "On a unification problem related to Kreisel's conjecture", Commentationes Mathematicae Universitatis Carolinae, Prague, Czechoslovakia, 29, no. 3, pp. 551-556, 1988.
	18	P. Purdom, Detecting looping simplifications, on Rewriting techniques and applications, p.54-61, May 1987, Bordeaux, France
	19	[19] Statman, R., Private communication, August 1988.

CITED BY 6

	Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993
	Mads Tofte , Lars Birkedal, A region inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.724-767, July 1998
	Gerd G. Hillebrand , Paris C. Kanellakis , Harry G. Mairson , Moshe Y. Vardi, Tools for Datalog boundedness, Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.1-12, May 29-31, 1991, Denver, Colorado, United States
	Mads Tofte , Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.188-201, January 16-19, 1994, Portland, Oregon, United States
	Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Tom Schrijvers , Maurice Bruynooghe, Polymorphic algebraic data type reconstruction, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy