The complexity of type inference for higher-order lambda calculi

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The complexity of type inference for higher-order lambda calculi

Full text

Pdf (1.07 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Orlando, Florida, United States

Pages: 119 - 130

Year of Publication: 1991

ISBN:0-89791-419-8

Authors

Fritz Henglein	Courant Institute of Mathematical Sciences, New York University, New York, N.Y. and Computer Science Department, Utrecht University, 3508 TB Utrecht, The Netherlands
Harry G. Mairson	Computer Science Department, Brandeis University, Waltham, Massachusetts

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 29, 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/99583.99602 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.

	Car89	L. Cardelli. Typeful programming. Lecture Notes for the IFIP Advanced Seminar on Formal Methods in Programming Language Semantics, Rio de Janeiro, Brazil, 1989. See also SRC Report 45, Digital Equipment Corporation.
	Dam85	L. Damas. Type assignment in programming languages. Ph.D. dissertation, CST- 33-85, Computer Science Department, Edinburgh University, 1985.
	DM82	Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
	DKM84	Cynthia Dwork , Paris C. Kanellakis , John C. Mitchell, On the sequential nature of unification, Journal of Logic Programming, v.1 n.1, p.35-50, June 1984 [doi>10.1016/0743-1066(84)90022-0]
	Edi88	Edinburgh University. Postgraduate Examination Que~tion~ in Computation Theory, 1978-1988. Laboratory for Foundations of Computer Science, Report ECS- LFCS-88-64.
	GR88	P. Giannini and S. Ronchi Della Rocca. Characterization of typings in polymorphic type discipline. In Proceedings of the 3-rd IEEE Symposium on Logic in Computer Science, pp. 61-70, July 1988.
	Gir72	J.-Y. Girard. Interprdtation Fonc. lionelle el Elimination des Coupures de l'Arilhmelique d'Ordre Superieur. Th~se de Doctorat d'Etat, Universit~ de Paris VII, 1972.
	GLT89	Jean-Yves Girard , Paul Taylor , Yves Lafont, Proofs and types, Cambridge University Press, New York, NY, 1989
	HMT90	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	HS65	J. Hartmanis and R. E. Stearns. On the computational complexity of algorithms. Transactions of the American Mathematieal Society 117, pp. 285-306.
	Hen90	F. Henglein. A lower bound for fult polymorphic type inference: Girard/Reynolds typability is DEXPTIME-hard. University of Utrecht, Technical Report RUU-CS-90- 14, April 1990.
	Hin69	1%. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146:29-60, 1969.
	HU79	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	HW88	P. Hudak and P. L. Wadler, editors. Report on the functional programming language Haskell. Yale University Technical Report YALEU/DCS/RR656, 1988.
	KM89	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]
	KMM90	P.C. Kanellakis, H. G. Mairson, and J. C. Mitchell. Unification and ML type reconstruction. In Computational Logic: Essays in Honor of Alan Robinson, ed. j.-L. Lassez and G. Plotkin. MIT Press, 1990.
	KTU90	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, ML typability is Dexptime-complete, Proceedings of the fifteenth colloquium on CAAP'90, p.206-220, May 1990, Copenhagen, Denmark
	KT89	A.J. Kfoury and j. Tiuryn. Type reconstruction in finite rank fragments of the second-order lambda calculus. Technical Report BUCS 89-011, Boston University, October 1989. Also in Proceedings of the 5-th IEEE Symposium on Logic in Computer Science, pp. 2-11, June 1990.
	Lan66	P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
	Mai90	Harry G. Mairson, Deciding ML typability is complete for deterministic exponential time, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.382-401, December 1989, San Francisco, California, United States [doi>10.1145/96709.96748]
	Mil78	R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, pp. 348-375, 1978.
	Mit90	John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	PW78	M.S. Paterson and M. N. Wegman. Linear unification. Journal of Computer and System Sciences 16, pp. 158-167, 1978.
	PDM89	B. Pierce, S. Dietzen, and S. Michaylov. Programming in higher-order typed lambda calculi. Technical Report CMU-CS-89- 111, Carnegie Mellon University, March 1989.
	PL89	Frank Pfenning , Peter Lee, LEAP: A Language with Eval And Polymorphism, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.345-359, March 13-17, 1989
	Rey74	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	Rob65	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	Sch82	H. Schwictenberg. Complexity of normalization in the pure typed lambda calculus. The L. E. J. Brouwer Centenary Symposium, A. S. Troelstra and D. van Daalen (eds.), pp. 453-457. North- Holland, 1982.
	Sco77	Dana S. Scott, Logic and programming languages, Communications of the ACM, v.20 n.9, p.634-641, Sept. 1977 [doi>10.1145/359810.359826]
	Str73	C. Strachey. The varieties of programming language. Technical Monograph PRG- 10, Programming Research Group, Oxford University, 1973.
	Tur85	D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France
	Wan87	M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae 10 (1987).

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
	Benjamin C. Pierce, Type systems, Programming methodology, Springer-Verlag New York, Inc., New York, NY, 2003
	A. J. Kfoury , J. Tiuryn , P. Urzyczyn, An analysis of ML typability, Journal of the ACM (JACM), v.41 n.2, p.368-398, March 1994
	Michael R. Fellows, Parameterized complexity: the main ideas and connections to practical computing, Experimental algorithmics: from algorithm design to robust and efficient software, Springer-Verlag New York, Inc., New York, NY, 2002
	Daniel Damian , Olivier Danvy, CPS transformation of flow information, Part II: administrative reductions, Journal of Functional Programming, v.13 n.5, p.925-933, September 2003
	David Van Horn , Harry G. Mairson, Relating complexity and precision in control flow analysis, ACM SIGPLAN Notices, v.42 n.9, September 2007