Abstract types have existential types

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	[Arbib and Manes 75] Arbib, M. A. and E. G. Manes, Arrows, Structures, and Functors: The Categorical Imperative. Academic Press 1975.
	2	[Barendregt 81] Barendregt. H. P, The Lambda Calculus: Its Syntax and Semantics. North Holland 1981.
	3	[Bates and Constable 81] Bates, J. L., and Robert L. Constable. The definition of µprl. Cornell Univ., Dept. of Computer Science technical report TR 82-492, October, 1981.
	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	[Burstall 84] Burstall, R. M., Programming with modules as typed functional programming. In Int. Conf. 5-th Generation Computing Systems. Nov., 1984.
	6	R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
	7	[Constable 80] Constable, Robert L., Programs and types. In 21st IEEE Symp. on Foundations of Computer Science. IEEE 1980, pages 118-128.
	8	[Coquand and Huet 84] Coquand, T. and Huet, G., A Theory of Constructions. In Proc. Int'l Symp. on Semantics of Data Types. June, 1984. Paper does not appear in proceedings.
	9	[Curry and Feys 58] Curry, H. B and Feys, R., Combinatory Logic I. North-Holland 1958.
	10	[DeBruijn 80] De Bruijn, N. G., A survey of the project AUTOMATH. In To H. B. Curry: Essays on Combinatory Loic, Lambda Calculus and Formalism. pages 579- 607. Academic Press 1980.
	11	Alan J. Demers , James E. Donahue, Data types, parameters and type checking, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-23, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567448]
	12	Alan Demers , James Donahue, "Type-completeness" as a language principle, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-244, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567469]
	13	Alan Demers , James Donahue , Glenn Skinner, Data types as values: polymorphism, type-checking, encapsulation, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.23-30, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512764]
	14	[DOD 80] US Dept. of Defense, Reference Manual for the Ada Programming Language. GPO 008-000-00354-8 1980.
	15	[Donahue 79] Donahue, J., On the semantics of data type. SIAM J. Computing 8 1979. pages 546-560.
	16	[Fitting 69] Fitting, M.C., Intuitionistic Logic. Model Theory and Forcing. North Holland 1969.
	17	Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
	18	[Gardner] Gardner, A., Search. A section of the Handbook of Artificial Intellegence, Barr and Feigenbaum (eds.)
	19	[Girard 71] Girard, J.-Y., Une extension de l'interpretation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analysc et la théorie des types. In Fenstad, J. E. (ed.), 2nd Scandinavian Logic Symp. pages 63- 92. North-Holland 1971.
	20	[Gordon, et. al. 79] Gordon, M.J., R. Milner and C.P. Wadsworth, Edinburgh LCF. Lecture Notes in Computer Science, Vol. 78 Springer-Verlag 1979.
	21	[Gratzer 68] Gratzer, G.. Universal Algebra. Van Nostrand 1968.
	22	John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
	23	Christopher T. Haynes, A theory of data type representation independence., Proc. of the international symposium on Semantics of data types, p.157-175, July 1984, Sophia-Antipolis, France
	24	[Herrlich and Strecker 73] Herrlich, H. and G.E. Strecker, Category Theory. Allyn and Bacon 1973.
	25	James G. Hook, Understanding Russell–a first attempt, Proc. of the international symposium on Semantics of data types, p.69-85, July 1984, Sophia-Antipolis, France
	26	[Howard 80] Howard, W., The formulas-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. pages 479- 490. Academic Press 1980.
	27	[Kapur 80] Kapur, D., Towards a Theory for Abstract Data Types. Massachusetts Institute of Technology technical report MIT/LCS/TM-237, 1980.
	28	[Lambek 80] Lambek, J., From Lambda Calculus to Cartesian Closed Categories. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. pages 375- 402. Academic Press 1980.
	29	[Lauchli 65] Lauchli, H., Intuitionistic propositional calculus and definably non-empty terms. Journal of Symbolic Logic 30 1965. pages 263.
	30	[Lauchli 70] Lauchli, H., An abstract notion of realizability for which intuitionistic predicte calculus is complete. In Intuitionism and Proof Theory: Proc. of the Summer Conference at Buffalo N.Y., 1970. pages 227-234.
	31	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]
	32	B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
	33	Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
	34	[Mac Lane 71] Mac Lane, S., Categories for the Working Mathematician. Graduate Texts in Mathematics, Vol. 5 Springer-Verlag 1971.
	35	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]
	36	[Martin-Löf 79] Martin-Löf, P., Constructive mathematics and computer programming. 1979. Paper presented at 6th International Congress for Logic, Methodology and Philosophy of Science, Preprint, Univ. of Stockholm, Dept. of Math. 1979.
	37	[McCracken 79] McCracken, N., An Investigation of a Programming Language with a Polymorphic Type Structure. Syracuse Univ. 1979.
	38	Nancy McCracken, The typechecking of programs with implicit type structure., Proc. of the international symposium on Semantics of data types, p.301-315, July 1984, Sophia-Antipolis, France
	39	[Mitchell, James G. et. al. 79] Mitchell, James G., Mayberry, W. and Sweet, R.. Mesa Language Manual. Xerox PARC technical report CSL-79-3, 1979.
	40	John Mitchell, Type inference and type containment., Proc. of the international symposium on Semantics of data types, p.257-277, July 1984, Sophia-Antipolis, France
	41	[Mitchell 84c] Mitchell, J.C., Semantic Models for Second-Order Lambda Calculus. In Proc. 25-th IEEE Symp. on Foundations of Computer Science. 1984, pages 289-299.
	42	James H. Morris, Jr., Types are not sets, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.120-124, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512938]
	43	Michael O'Donnell, A programming language theorem which is independent of Peano Arithmetic, Proceedings of the eleventh annual ACM symposium on Theory of computing, p.176-188, April 30-May 02, 1979, Atlanta, Georgia, United States [doi>10.1145/800135.804411]
	44	[Prawitz 65] Prawitz, D., Natural Deduction. Almquist and Wiksell Stockholm 1965.
	45	[Prawitz 71] Prawitz, D., Ideas and Results in Proof Theory. In Fenstad, J.E. (ed.), 2nd Scandinavian Logic Symp. pages 235-308. North-Holland 1971.
	46	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	47	[Reynolds 81a] Reynolds, J.C., The Essence of ALGOL. In de Bakker and van Vliet (ed.), Inter. Symp. on Algorithmic Languages. North Holland 1981. pages 345-372.
	48	John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
	49	[Reynolds 83] Reynolds, J.C., Types, Abstraction, and Parametric Polymorphism. In IFIP Congress. 1983, pages.
	50	[Reynolds 84] Reynolds, J.C., Polymorphism is not Set-Theoretic. In Int. Symp. on Semantics of Data Types. Springer-Verlag 1984. pages 145-156.
	51	[Shaw 81] Shaw, M. (ed.). ALPHARD: Form and Content. Springer-Verlag 1981.
	52	[Sherman et. al. 82] Sherman, M.. Higsen. A. and Rosenberg, J., A Methodology for programming abstract data types in Ada. In Proc. AdaTec Conf. on Ada. 1982. pages 66-75.
	53	[Statman 79] Statman, R., Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoretical Computer Science 9 1979. pages 67-72.
	54	[Stenlund 72] Stenlund, S., Combinators. ¿-terms and Proof Theory. Reidel Dordrecht-Holland 1972.
	55	[Troelstra 73] Troelstra, A.S., Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, Vol. 344 Springer-Verlag 1973.
	56	[Wulf et. al. 76] Wulf, W.W., R. London, and M. Shaw, An introduction to the construction and verification of Alphard programs. IEEE Trans. on Software Engineering SE-2 1976. pages 253-264.