On the type structure of standard ML

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

On the type structure of standard ML

Full text

Pdf (2.68 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 15 , Issue 2 (April 1993) table of contents

Pages: 211 - 252

Year of Publication: 1993

ISSN:0164-0925

Authors

Robert Harper	Carnegie Mellon Univ., Pittsburgh, PA
John C. Mitchell	Stanford Univ., Stanford, CA

Publisher

ACM New York, NY, USA

Bibliometrics

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

Additional Information:

references cited by index terms review 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/169701.169696 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	AMADIO, R., BRUCE, K., AND LONGO, G. The finitary projection model for second order lambda calculus and solutions to higher order domain equations. In Proceedings of the IEEE OEvmpostum on Logic in Computer Science, (1986), 122-130.
	2	BARENDREG, H.P. The Lambda Calculus: frs Syntax and Semantics. 2nd ed. North-Holland, Amsterdam, 1984.
	3	Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
	4	Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
	5	Kim B. Bruce , Albert R. Meyer , John C. Mitchell, The semantics of second-order lambda calculus, Information and Computation, v.85 n.1, p.76-134, March 1990 [doi>10.1016/0890-5401(90)90044-I]
	6	Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
	7	L. Cardelli, Structural subtyping and the notion of power type, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.70-79, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73566]
	8	Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985 [doi>10.1145/6041.6042]
	9	Robert Cartwright, Types as intervals, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.22-36, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318604]
	10	R L Constable, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	11	COQUAND, T. An analysis of Girard's paladox. In Proceedings of the IEEE Symposium on Logic in Computer Science (June 1986), 227 236.
	12	Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
	13	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]
	14	DE BRUIJN, N. G. A survey of the project Automath. In Te H B. Curry: Essays on Combmatory Logtc, Lambda Calculus and FormaDsm. Academic Press, New York, 1980, 579 607.
	15	GIRARD, J.-Y. Interpretation fonctlonelle et eliminatlon des coupures de l'arithmetique d'ordre superieur. These D'Etat, Umversite Paris VII, 1972.
	16	GmARD, J-Y. Une extension de l'interpretation de Godel ~ l'analyse, et son application ~ l'~hmmation des coupures dans l'analyse et la th~orie des types. In 2nd Scandmavmn Logtc Syrnposntm, J. E. Fenstad, Ed., (North-Holland, Amsterdam, 1971), 63 92.
	17	GORDON, M. J., MmN~~, R., AND WADSWORTH C. P. Edznburgh LCF. LNCS 78, Springer, Berhn, 1979
	18	HARPER, R., HONSELL, F., AND PLOTKIN, G. A framework for defining logics. In Proceedings of the IEEE Sympostum on Log~c zn Computer Sctence (June 1987), 194-204. Te appear m J. ACM.
	19	HARPER, R., MAcQUEEN, D. B., AND MILNER, R Standard ML Tech. Rep. ECS-LFCS-8"-2, Lab. for Foundations of Computer Science, Univ. of Edinburgh, Mat. 1986.
	20	R. Harper , R. Milner , M. Tofte, A type discipline for Program modules, II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development, p.308-319, March 1987, Pisa, Italy
	21	Robert Harper , John C. Mitchell , Eugenio Moggi, Higher-order modules and the phase distinction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.341-354, December 1989, San Francisco, California, United States [doi>10.1145/96709.96744]
	22	James G. Hook , Douglas J. Howe, Impredicative Strong Existential Equivalent to Type:Type, Cornell University, Ithaca, NY, 1986
	23	HOWARD, W. The formulas-as-types notion of construction. In Te H. B. Curry: Essays on Combznatorv Logzc, Lambda-Calculus and Formahsm Academic Press, 1980, 479 490.
	24	HOWE, D.J. The computational behavior of Girard's paradox. In Proceedtngs of the IEEE Symposium on Logtc ~n Computer Science (June 1987), 205 214.
	25	K~ELL^K~S, P. C., MAmSON, H G., AND MITCHELL, J. C. Unificatmn and ML type reconstructmn In Computattonal Log~c, Essays zn Honor of Alan Robmson. MIT Press, 1991, 444 478.
	26	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
	27	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]
	28	David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
	29	David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
	30	David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
	31	MARTIN-L~F, P. An intuitionistic theory of types: Pred~chve part. In H. E. Rose and J. C. Shepherdson, Eds. Logtc Colloqutum, '73, Amsterdam, 1973, North-Holland, 73-118.
	32	M^RTIN-L"F, P. Constructive mathematics and computer progTamming In S~xth International Congress for Logtc, Methodology, and Phdosophy of Science North-Holland, Amsterdam, 1982, 153 175
	33	MARTIN-L~F, P. lntultzomstlc Type Theo~2~. Bibliopolis, Napoh, 1984.
	34	Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
	35	A. R. Meyer , J. C. Mitchell , E. Moggi , R. Statman, Empty types in polymorphic lambda calculus, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.253-262, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41648]
	36	Albert R. Meyer , Mark B. Reinhold, "Type" is not a type, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.287-295, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512671]
	37	MILNER, R. A theory of type polymorphism in programming. JCSS, 17 (1978), 348-375.
	38	M~LNER, R. The Standard ML core language. Polymorphism 2, 2 (1985), 1-28. An earlier version appeared in Proceedings of the 1984 ACM Symposium on Lisp and Functional Programming.
	39	Robin Milner , Mads Tofte, Commentary on standard ML, MIT Press, Cambridge, MA, 1991
	40	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	41	John C. Mitchell, A type-inference approach to reduction properties and semantics of polymorphic expressions (summary), Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	42	John C. Mitchell, Polymorphic type inference and containment, Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	43	John C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.263-276, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512669]
	44	John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	45	John C. Mitchell , Albert R. Meyer, Second-Order Logical Relations (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.225-236, June 17-19, 1985
	46	MITCHELL, J. C., AND MOGG~, E. IG'ipke-style models for typed lambda calculus. Ann. Pure Appl. Logic 51 (1991), 99 124. Preliminary version in Proceedings of the IEEE Symposium on Logic in Computer Science (1987), 303 314.
	47	John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
	48	MOGGI, E. A category-theoretic account of progTam modules. Math. Structures Comput. Scz. 1, i (1991), 103-139.
	49	E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
	50	Atsushi Ohori, A simple semantics for ML polymorphism, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.281-292, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99393]
	51	PLOTmN, G.D. Calt-by-name, call-by-value and the lambda calculus. Theor. Comput. Sct. 1 (1975), 125-159.
	52	PLOTKIN, G.D. LCF considered as a progTamming language. Theor. Comput. Scz. 5 (1977), 223 255.
	53	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	54	REYNOLDS, J.C. The essence of Algol. In Algorithmzc Languages, de Bakker and van Vliet, Eds. IFIP, North-Holland, Amsterdam, 1981, 345-372.
	55	REYNOLD, J.C. Types, abstraction, and parametric polymorphism. In Informatzon Processing '83, North-Holland, Amsterdam, 1983, 513-523.
	56	REYNOLDS, J. C. Polymorphism is not set-theoretic. In Proceedings of the Internattonal Symposium on Semantics of Data Types (Sophia-Antirolis, France), LNCS 173, Springer, Berlin, 1984, 145-156.
	57	SCOTT, D. S. Relating theories of the lambda calculus. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980, 403-450.
	58	SEEL~, R. A. G. Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc. 95 (1984), 33-48.
	59	SEELY, R. A. G. Categorical semantics for higher-order polymorphic lambda calculus. J. Symbolic Logic 52 (1987), 969-989.
	60	STATiVlAN, R. Logical relations and the typed lambda calculu~. Ir~f. Control 65 (1985), 86 97.
	61	Allen Stoughton, Fully abstract models of programming languages, Pitman Publishing, Inc., Marshfield, MA, 1988
	62	TROELSTRA, M. Mathemat~cal investigation of intuitiomstic arithmetic and analysis. LNM $44~ Springer, Berlin, 1973.
	63	TOFTE, M. Operational semantics and polymorphic type inference. Ph.D. dissertatlon~ Edinburgh Univ, 1988. Avafiable as Edinburgh Univ. Laboratory for Foundatlons of Computer Science Tech Rep. ECS-LFCS-88-54
	64	Mitchell Wand, A types-as-sets semantics for milner-style polymorphism, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.158-164, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800527]

CITED BY 29

	Sandip K. Biswas, Higher-order functors with transparent signatures, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-163, January 23-25, 1995, San Francisco, California, United States
	Robert Harper , Mark Lillibridge, Explicit polymorphism and CPS conversion, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-219, March 1993, Charleston, South Carolina, United States
	Zhong Shao, Transparent modules with fully syntatic signatures, ACM SIGPLAN Notices, v.34 n.9, p.220-232, Sept. 1999
	Karl Crary , Robert Harper , Sidd Puri, What is a recursive module?, ACM SIGPLAN Notices, v.34 n.5, p.50-63, May 1999
	Fritz Henglein , Jesper Jørgensen, Formally optimal boxing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.213-226, January 16-19, 1994, Portland, Oregon, United States
	Atsushi Ohori, A polymorphic record calculus and its compilation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.6, p.844-895, Nov. 1995
	Xavier Leroy, Applicative functors and fully transparent higher-order modules, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-153, January 23-25, 1995, San Francisco, California, United States
	Zhong Shao, Flexible representation analysis, ACM SIGPLAN Notices, v.32 n.8, p.85-98, Aug. 1997
	Andrew Tolmach, Tag-free garbage collection using explicit type parameters, ACM SIGPLAN Lisp Pointers, v.VII n.3, p.1-11, July-Sept. 1994
	Atsushi Ohori , Nobuaki Yoshida, Type inference with rank 1 polymorphism for type-directed compilation of ML, ACM SIGPLAN Notices, v.34 n.9, p.160-171, Sept. 1999
	François Bourdoncle , Stephan Merz, Type checking higher-order polymorphic multi-methods, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.302-315, January 15-17, 1997, Paris, France
	Dominic Duggan, Dynamic typing for distributed programming in polymorphic languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.1, p.11-45, Jan. 1999
	Simon Peyton Jones , Mark Shields , John Launchbury , Andrew Tolmach, Bridging the gulf: a common intermediate language for ML and Haskell, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 19-21, 1998, San Diego, California, United States
	Ferruccio Damiani, Rank 2 intersection types for modules, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.67-78, August 27-29, 2003, Uppsala, Sweden
	Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States
	Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States
	Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Matthew Fluet , Stephen Weeks, Contification using dominators, ACM SIGPLAN Notices, v.36 n.10, October 2001
	Atsushi Ohori , Tomonobu Takamizawa, An Unboxed Operational Semantics for ML Polymorphism, Lisp and Symbolic Computation, v.10 n.1, p.61-91, June 1997
	Claudio V. Russo, First-class structures for standard ML, Nordic Journal of Computing, v.7 n.4, p.348-374, Winter 2000
	Zhong Shao, Typed cross-module compilation, ACM SIGPLAN Notices, v.34 n.1, p.141-152, Jan. 1999
	Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States
	Zhong Shao, Typed common intermediate format, Proceedings of the Conference on Domain-Specific Languages on Conference on Domain-Specific Languages (DSL), 1997, p.8-8, October 15-17, 1997, Santa Barbara, California
	Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
	Martin Sulzmann , Meng Wang, Modular generic programming with extensible superclasses, Proceedings of the 2006 ACM SIGPLAN workshop on Generic programming, September 16-16, 2006, Portland, Oregon, USA
	William L. Harrison , Richard B. Kieburtz, The logic of demand in Haskell, Journal of Functional Programming, v.15 n.6, p.837-891, November 2005
	Philippe Narbel, Type sharing constraints and undecidability, Journal of Functional Programming, v.17 n.2, p.207-214, March 2007
	Gilles Barthe, Type-checking injective pure type systems, Journal of Functional Programming, v.9 n.6, p.675-698, November 1999
	Gilles Barthe , John Hatcliff , Morten Heine B. Sørensen, CPS Translations and Applications: The Cube and Beyond, Higher-Order and Symbolic Computation, v.12 n.2, p.125-170, September 1999

INDEX TERMS

Primary Classification:
F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS
F.3.3 Studies of Program Constructs
Subjects: Type structure

Additional Classification:
D. Software
D.3 PROGRAMMING LANGUAGES
D.3.2 Language Classifications
Subjects: Applicative (functional) languages
Nouns: ML
D.3.3 Language Constructs and Features
Subjects: Abstract data types; Modules, packages

F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS
F.3.2 Semantics of Programming Languages
Subjects: Operational semantics; Denotational semantics
F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
F.4.1 Mathematical Logic
Subjects: Lambda calculus and related systems

General Terms:
Design, Languages, Theory

REVIEW

"Pierre Weis : Reviewer"

A framework for a formal description of the type checking and semantics of the core of the Standard ML purely functional language and its module system is presented in this research paper. The formalism is based on an explicitly typed second-o more...

Collaborative Colleagues:

Robert Harper: colleagues

John C. Mitchell: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player