Article

Free access

Abstract types have existential types

Authors:

John C. Mitchell,

Gordon D. PlotkinAuthors Info & Claims

POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 37 - 51

https://doi.org/10.1145/318593.318606

Published: 01 January 1985 Publication History

PDF eReader

References

[1]

{Arbib and Manes 75} Arbib, M. A. and E. G. Manes, Arrows, Structures, and Functors: The Categorical Imperative. Academic Press 1975.

Google Scholar

[2]

{Barendregt 81} Barendregt. H. P, The Lambda Calculus: Its Syntax and Semantics. North Holland 1981.

Google Scholar

[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.

Google Scholar

[4]

{Bruce and Meyer 84} Bruce, K. and Meyer, A., A Completeness Theorem for Second-Order Polymorphic Lambda Calculus. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France). 1984, pages 131-144.

Digital Library

Google Scholar

[5]

{Burstall 84} Burstall, R. M., Programming with modules as typed functional programming. In Int. Conf. 5-th Generation Computing Systems. Nov., 1984.

Google Scholar

[6]

{Burstall and Lampson 84} Burstall, R. and Lampson, B., A Kernel Language for Abstract Data Types and Modules. In Proc. Int'l Symp. on Semantics of Data Types. 1984, pages 1-50.

Digital Library

Google Scholar

[7]

{Constable 80} Constable, Robert L., Programs and types. In 21st IEEE Symp. on Foundations of Computer Science. IEEE 1980, pages 118-128.

Digital Library

Google Scholar

[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.

Google Scholar

[9]

{Curry and Feys 58} Curry, H. B and Feys, R., Combinatory Logic I. North-Holland 1958.

Google Scholar

[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.

Google Scholar

[11]

{Demers and Donahue 80a} Demers, A. J. and J. E. Donahue, Data types, parameters and type checking. In 7th ACM Symp. on Principles of Programming Languages. ACM 1980, pages 12-23.

Digital Library

Google Scholar

[12]

{Demers and Donahue 80b} Demers, A. J. and J. E. Donahue, 'Type-completeness' as a language principle. In 7th ACM Symp. on Principles of Programming Languages. ACM 1980, pages 234-244.

Digital Library

Google Scholar

[13]

{Demers et. al. 78} Demers, A., J. Donahue and G. Skinner, Data types as values: polymorphism, type-checking, encapsulation. In 5th ACM Symp. on Principles of Programming Languages. ACM 1978, pages 23-30.

Digital Library

Google Scholar

[14]

{DOD 80} US Dept. of Defense, Reference Manual for the Ada Programming Language. GPO 008-000-00354-8 1980.

Google Scholar

[15]

{Donahue 79} Donahue, J., On the semantics of data type. SIAM J. Computing 8 1979. pages 546-560.

Google Scholar

[16]

{Fitting 69} Fitting, M.C., Intuitionistic Logic. Model Theory and Forcing. North Holland 1969.

Google Scholar

[17]

{Fortune, et. al. 83} Fortune, S., Leivant, D. and O'Donnel. M., The Expressiveness of Simple and Second Order Type Structures. JACM 30. 1 1983. pages 151-185.

Digital Library

Google Scholar

[18]

{Gardner} Gardner, A., Search. A section of the Handbook of Artificial Intellegence, Barr and Feigenbaum (eds.)

Google Scholar

[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.

Crossref

Google Scholar

[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.

Google Scholar

[21]

{Gratzer 68} Gratzer, G. Universal Algebra. Van Nostrand 1968.

Google Scholar

[22]

{Guttag, et. al. 78} Guttag, J.V., E. Horowitz and D.R. Musser, Abstract data types and software validation. Comm. ACM 21, 12 1978. pages 1048-1064.

Digital Library

Google Scholar

[23]

{Haynes 84} Haynes, C.T., A Theory of Data Type Representation Independence. In Int. Symp. on Semantics of Data Types. Springer-Verlag 1984, pages 157-176.

Digital Library

Google Scholar

[24]

{Herrlich and Strecker 73} Herrlich, H. and G.E. Strecker, Category Theory. Allyn and Bacon 1973.

Google Scholar

[25]

{Hook 84} Hook, J.G., Understanding Russell - A First Attempt. In Int. Symp. on Semantics of Data Types. Springer-Verlag 1984, pages 69-85.

Digital Library

Google Scholar

[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.

Google Scholar

[27]

{Kapur 80} Kapur, D., Towards a Theory for Abstract Data Types. Massachusetts Institute of Technology technical report MIT/LCS/TM-237, 1980.

Google Scholar

[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.

Google Scholar

[29]

{Lauchli 65} Lauchli, H., Intuitionistic propositional calculus and definably non-empty terms. Journal of Symbolic Logic 30 1965. pages 263.

Google Scholar

[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.

Crossref

Google Scholar

[31]

{Leivant 83a} Leivant, D., Polymorphic Type Inference. In Proc. 10-th ACM Symp. on Principles of Programming Languages. 1983, pages 88-98.

Digital Library

Google Scholar

[32]

{Liskov et. al. 81} Liskov, B. et. al., CLU Reference Manual. Lecture Notes in Computer Science, Vol. 114 Springer-Verlag 1981.

Digital Library

Google Scholar

[33]

{Liskov et. al. 77} Liskov, B. A. Snyder, R. Atkinson and C. Schaffert, Abstraction mechanisms in CLU. Comm. ACM 20 1977. pages 564-576.

Digital Library

Google Scholar

[34]

{Mac Lane 71} Mac Lane, S., Categories for the Working Mathematician. Graduate Texts in Mathematics, Vol. 5 Springer-Verlag 1971.

Google Scholar

[35]

{MacQueen 84} MacQueen, D.B., Modules for Standard ML. In ACM Symp. on Lisp and Functional Programming. 1984. pages 198-207.

Digital Library

Google Scholar

[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.

Google Scholar

[37]

{McCracken 79} McCracken, N., An Investigation of a Programming Language with a Polymorphic Type Structure. Syracuse Univ. 1979.

Google Scholar

[38]

{McCracken 84} McCracken, N., The Typechecking of Programs with Implicit Type Structure. In Proc. Int'l Symp. on Semantics of Data Types. June, 1984, pages 301-316.

Digital Library

Google Scholar

[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.

Google Scholar

[40]

{Mitchell 84b} Mitchell, J.C., Type Inference and Type Containment. In Proc. Int'l Symp. on Semantics of Data Types. June, 1984. pages 257-278.

Digital Library

Google Scholar

[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.

Google Scholar

[42]

{Morris 73} Morris, James H., Types are not sets. In 1st ACM Symp. on Principles of Programming Languages. ACM 1973, pages 120-124.

Digital Library

Google Scholar

[43]

{ODonnell 79} O'Donnell, M., A practical programming theorem which is independent of Peano arithmetic. In 11th ACM Symp. on the Theory of Computation. ACM 1979, pages 176-188.

Digital Library

Google Scholar

[44]

{Prawitz 65} Prawitz, D., Natural Deduction. Almquist and Wiksell Stockholm 1965.

Google Scholar

[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.

Crossref

Google Scholar

[46]

{Reynolds 74} Reynolds, J.C., Towards a Theory of Type Structure. In Paris Colloq. on Programming. Springer-Verlag 1974, pages 408-425.

Digital Library

Google Scholar

[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.

Google Scholar

[48]

{Reynolds 81b} Reynolds. J.C., The Craft of Programming. Prentice Hall 1981.

Digital Library

Google Scholar

[49]

{Reynolds 83} Reynolds, J.C., Types, Abstraction, and Parametric Polymorphism. In IFIP Congress. 1983, pages.

Google Scholar

[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.

Crossref

Google Scholar

[51]

{Shaw 81} Shaw, M. (ed.). ALPHARD: Form and Content. Springer-Verlag 1981.

Google Scholar

[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.

Digital Library

Google Scholar

[53]

{Statman 79} Statman, R., Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoretical Computer Science 9 1979. pages 67-72.

Google Scholar

[54]

{Stenlund 72} Stenlund, S., Combinators. ¿-terms and Proof Theory. Reidel Dordrecht-Holland 1972.

Google Scholar

[55]

{Troelstra 73} Troelstra, A.S., Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, Vol. 344 Springer-Verlag 1973.

Google Scholar

[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.

Digital Library

Google Scholar

Cited By

View all

Clement BRémy DRadanne G(2024)Fulfilling OCaml Modules with TransparencyProceedings of the ACM on Programming Languages10.1145/36498188:OOPSLA1(194-222)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649818
Coquand T(2023)Some Remarks About Dependent Type TheoryThe French School of Programming10.1007/978-3-031-34518-0_8(175-202)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_8
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Show More Cited By

Index Terms

Abstract types have existential types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs

Recommendations

On subtyping, wildcards, and existential types
FTfJP '09: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs

Wildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow '...
Contractive signatures with recursive types, type parameters, and abstract types
ICALP'13: Proceedings of the 40th international conference on Automata, Languages, and Programming - Volume Part II

Although theories of equivalence or subtyping for recursive types have been extensively investigated, sophisticated interaction between recursive types and abstract types has gained little attention. The key idea behind type theories for recursive types ...
Qualified types for MLF
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming

MLF is a type system that extends a functional language with impredicative rank-n polymorphism. Type inference remains possible and only in some clearly defined situations, a local type annotation is required. Qualified types are a general concept that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '85: Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1985

340 pages

ISBN:0897911474

DOI:10.1145/318593

Chairmen:
Mary S. Van Deusen
IBM Watson Research
,
Zvi Galil
Columbia University, New York, NY
,
Brian K. Reid
Stanford Univ., Stanford, CA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1985

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

79
Total Citations
View Citations
458
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)7

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Clement BRémy DRadanne G(2024)Fulfilling OCaml Modules with TransparencyProceedings of the ACM on Programming Languages10.1145/36498188:OOPSLA1(194-222)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649818
Coquand T(2023)Some Remarks About Dependent Type TheoryThe French School of Programming10.1007/978-3-031-34518-0_8(175-202)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_8
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Cutler JLicata DDanner N(2020)Denotational recurrence extraction for amortized analysisProceedings of the ACM on Programming Languages10.1145/34089794:ICFP(1-29)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408979
New MJamner DAhmed A(2019)Graduality and parametricity: together again for the first timeProceedings of the ACM on Programming Languages10.1145/33711144:POPL(1-32)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371114
Peyton Jones MGkoumas VKireev RMacKenzie KNester CWadler P(2019)Unraveling Recursion: Compiling an IR with Recursion to System FMathematics of Program Construction10.1007/978-3-030-33636-3_15(414-443)Online publication date: 20-Oct-2019
https://doi.org/10.1007/978-3-030-33636-3_15
Sekiyama TIgarashi AGreenberg M(2017)Polymorphic Manifest Contracts, Revised and ResolvedACM Transactions on Programming Languages and Systems10.1145/299459439:1(1-36)Online publication date: 6-Feb-2017
https://dl.acm.org/doi/10.1145/2994594
Feferman S(2016)Turing's ‘Oracle’: From Absolute to Relative Computability and BackThe Once and Future Turing10.1017/CBO9780511863196.020(300-334)Online publication date: 5-Mar-2016
https://doi.org/10.1017/CBO9780511863196.020
(2016)Oracles, Infinitary Computation, and the Physics of the MindThe Once and Future Turing10.1017/CBO9780511863196.019(297-299)Online publication date: 5-Mar-2016
https://doi.org/10.1017/CBO9780511863196.019
Dinsdale-Young TGardner PWheelhouse M(2011)Abstract local reasoning for program modulesProceedings of the 4th international conference on Algebra and coalgebra in computer science10.5555/2040096.2040100(36-39)Online publication date: 30-Aug-2011
https://dl.acm.org/doi/10.5555/2040096.2040100
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

On subtyping, wildcards, and existential types

Contractive signatures with recursive types, type parameters, and abstract types

Qualified types for MLF