Principality and decidable type inference for finite-rank intersection types

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Principality and decidable type inference for finite-rank intersection types

Full text

Pdf (1.70 MB)

Source

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

San Antonio, Texas, United States

Pages: 161 - 174

Year of Publication: 1999

ISBN:1-58113-095-3

Authors

A. J. Kfoury	Boston University, Boston, MA
J. B. Wells	Heriot-Watt University, EDINBURGH, EH14 4AS, Scotland

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): 3, Downloads (12 Months): 22, Citation Count: 13

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/292540.292556 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.

	vB93	S. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Catholic University of Nijmegen, 1993.
	Ban97	Anindya Banerjee, A modular, polyvariant and type-based closure analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.1-10, June 09-11, 1997, Amsterdam, The Netherlands
	CDCV80	M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and A-calculus semantics. In Seldin and Hindley {SH80}, pp. 535-560.
	CDCV81	M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Z. Math. Log. Grund. Math., 27:45-58, 1981.
	CG92	Mario Coppo , Paola Giannini, A Complete Type Inference Algorithm for Simple Intersection Types, Proceedings of the 17th Colloquium on Trees in Algebra and Programming, p.102-123, February 26-28, 1992
	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]
	GJS96	James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	Jen98	Thomas P. Jensen, Inference of polymorphic and conditional strictness properties, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.209-221, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268964]
	Jim96	Trevor Jim, What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-53, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237728]
	JMZ92	Bart Jacobs , Ines Margaria , Maddalena Zacchi, Filter models with polymorphic types, Theoretical Computer Science, v.95 n.1, p.143-158, March 23, 1992 [doi>10.1016/0304-3975(92)90070-V]
	Kfo9X	A. J. Kfoury. Beta-reduction as unification. In D. Niwinski, ed., Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference, December 1996). Springer-Verlag, 199X.
	KW94	A. J. Kfoury , J. B. Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order &lgr;-calculus, Proceedings of the 1994 ACM conference on LISP and functional programming, p.196-207, June 27-29, 1994, Orlando, Florida, United States
	Lei83	Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567077]
	MTHM90	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	Pie94	Benjamin C. Pierce, Bounded quantification is undecidable, Information and Computation, v.112 n.1, p.131-165, July 1994 [doi>10.1006/inco.1994.1055]
	PJHH+93	S. L. Peyton Jones, C. Hall, K. Hammond, W. Partain, and P. Wadler. The Glasgow Haskell compiler: A technical overview. In Proc. UK Joint Framework .for Information Technology (JFIT) Technical Conf., 1993.
	Pot80	G. Pottinger. A type assignment for the strongly normalizable )~-terms. In Seldin and Hindley {SH80}, pp. 561-577.
	RDR88	S. Ronchi Della Rocca, Principal type scheme and unification for intersection type discipline, Theoretical Computer Science, v.59 n.1-2, p.181-209, July 1988 [doi>10.1016/0304-3975(88)90101-6]
	RDRV84	S. Ronchi Della Rocca and B. Venneri. Principal type schemes for an extended type theory. Theor. Cornp. Sc., 28:151-169, 1984.
	SH80	J.P. Seldin and J. R. Hindley, eds. To H. B. Curry: Essays on Cornbinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
	SM96	t~. Sayag and M. Mauny. A new presentation of the intersection type discipline through principal typings of normal forms. Technical Report RR-2998, INRIA, Oct. 16, 1996.
	SM97	I~. Sayag and M. Mauny. Structural properties of intersection types. In Proceedings of the 8th international Conference on Logic and Computer Science - Theoretical Foundations of Computing (LIRA), pp. 167-175, Novi Sad, Yugoslavia, Sept. 1997.
	Urz97	Paweł Urzyczyn, Type reconstruction in F _ω, Mathematical Structures in Computer Science, v.7 n.4, p.329-358, August 1997 [doi>10.1017/S0960129597002302]
	Wel94	J. B. Wells. Typability and type checking in the second-order A-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Syrnp. Logic in Computer Sci., 1994. Superseded by {WeI9X}.
	Wel96	J. B. Wells, Typability is Undecidable for F+Eta, Boston University, Boston, MA, 1996
	Wel9X	J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic, 199X. To appear. Supersedes {Wel94}.

CITED BY 13

	Xavier Leroy , François Pessaux, Type-based analysis of uncaught exceptions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.340-377, March 2000
	Assaf J. Kfoury , Harry G. Mairson , Franklyn A. Turbak , J. B. Wells, Relating typability and expressiveness in finite-rank intersection type systems (extended abstract), ACM SIGPLAN Notices, v.34 n.9, p.90-101, Sept. 1999
	Ferruccio Damiani, Rank 2 intersection types for local definitions and conditional expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.4, p.401-451, July 2003
	Didier Le Botlan , Didier Rémy, ML^F: raising ML to the power of system F, ACM SIGPLAN Notices, v.38 n.9, p.27-38, September 2003
	A. J. Kfoury , J. B. Wells, Principality and type inference for intersection types using expansion variables, Theoretical Computer Science, v.311 n.1-3, p.1-70, 23 January 2004
	Sébastien Carlier , J. B. Wells, Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.132-143, August 24-26, 2004, Verona, Italy
	Peter Møller Neergaard , Harry G. Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Antonio Bucciarelli , Adolfo Piperno , Ivano Salvo, Intersection types and λ-definability, Mathematical Structures in Computer Science, v.13 n.1, p.15-53, February 2003
	Anindya Banerjee , Thomas Jensen, Modular control-flow analysis with rank 2 intersection types, Mathematical Structures in Computer Science, v.13 n.1, p.87-124, February 2003
	Ferruccio Damiani, A conjunctive type system for useless-code elimination, Mathematical Structures in Computer Science, v.13 n.1, p.157-197, February 2003
	Mário Florido , Luís Damas, Linearization of the lambda-calculus and its relation with intersection type systems, Journal of Functional Programming, v.14 n.5, p.519-546, September 2004
	Viviana Bono , Betti Venneri , Lorenzo Bettini, A typed lambda calculus with intersection types, Theoretical Computer Science, v.398 n.1-3, p.95-113, May, 2008
	J. B. Wells , Allyn Dimock , Robert Muller , Franklyn Turbak, A calculus with polymorphic and polyvariant flow types, Journal of Functional Programming, v.12 n.3, p.183-227, May 2002