article

Open access

Abstract types have existential type

Editor: Susan L. Graham Authors:

John C. Mitchell,

Gordon D. PlotkinAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 10, Issue 3

Pages 470 - 502

https://doi.org/10.1145/44501.45065

Published: 01 July 1988 Publication History

PDF eReader

Abstract

Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite “value” we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.

References

[1]

ARBIB, M. A., AND MANES, E.G. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press, Orlando, Fla., 1975.

Google Scholar

[2]

BARENDREGT, H. P. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, The Netherlands, 1984 (revised edition).

Google Scholar

[3]

BRUCE, K. B., AND MEYER, A. A completeness theorem for second-order polymorphic lambda calculus. In Proceedings of the International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 131-144.

Crossref

Google Scholar

[4]

BRUCE, K. B., MEYER, A. R., AND MITCHELL, J. C. The semantics of second-order lambda calculus. In Information and Computation (to be published),

Crossref

Google Scholar

[5]

BURSTALL, R. M., AND GOGUEN, J. Putting theories together to make specifications. In Fifth International Joint Conference on Artificial Intelligence, 1977, pp. 1045-1958.

Google Scholar

[6]

BURSTALL, a. M., AND GOGUEN, J. An informal introduction to specification using CLEAR. In The Correctness Problem in Computer Science, Boyer and Moore, Eds. Academic Press, Orlando, Fla., 1981, pp. 185-213.

Google Scholar

[7]

BURSTALL, R., AND LAMPSON, B. A kernel language for abstract data types and modules. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 1-50.

Crossref

Google Scholar

[8]

CONSTABLE, R.L. Programs and types. In 21st IEEE Symposium on Foundations of Computer Science (Syracuse, N.Y., Oct. 1980). IEEE, New York, 1980, pp. 118-128.

Google Scholar

[9]

CONSTABLE, R. L., ET AL. Implementing Mathematics With The Nuprl Proof Development System. Graduate Texts in Mathematics, vol. 37, Prentice-Hall, Englewood Cliffs, N.J., 1986.

Crossref

Google Scholar

[10]

COQUAND, T. An analysis of Girard's paradox. In Proceedings of the IEEE Symposium on Logic in Computer Science (June 1986). IEEE, New York, 1986, pp. 227-236.

Google Scholar

[11]

COQUAND, T., AND HUET, G. The calculus of constructions. Inf. Comput. 76, 2/3 (Feb./Mar. 1988), 95-120.

Crossref

Google Scholar

[12]

CURRY, H. B., AND FEYS, R. Combinatory Logic L North-Holland, Amsterdam, 1958.

Google Scholar

[13]

DEBRUIJN, N. G. A survey of the project Automath. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 579-607.

Google Scholar

[14]

DEMERS, A. J., AND DONAHUE, J.E. Data types, parameters and type checking. In 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Nev., Jan. 28-30, 1980). ACM, New York, 1980, pp. 12-23.

Crossref

Google Scholar

[15]

DEMERS, A. J., AND DONAHUE, J.E. 'Type-completeness' as a language principle. In 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Nev., Jan. 28-30, 1980). ACM, New York, 1980, pp. 234-244.

Crossref

Google Scholar

[16]

DEMERS, A. J., DONAHUE, J. E., AND SKINNER, G. Data types as values: polymorphism, typechecking, encapsulation. In 5th ACM Symposium on Principles of Programming Languages (Tucson, Ariz., Jan. 23-25, 1978). ACM, New York, 1978, pp. 23-30.

Crossref

Google Scholar

[17]

U.S. DEPARTMENT OF DEFENSE Reference Manual for the Ada Programming Language. GPO 008-000-00354-8, 1980.

Google Scholar

[18]

DONAHUE, J. On the semantics of data type. SIAM J. Comput. 8 (1979), 546-560.

Google Scholar

[19]

FITTING, M. C. Intuitionistic Logic, Model Theory and Forcing. North-Holland, Amsterdam, 1969.

Google Scholar

[20]

FORTUNE, S., LEIVANT, D., AND O'DONNELL, M. The expressiveness of simple and second order type structures. J. ACM 30, I (1983), 151-185.

Crossref

Google Scholar

[21]

GIRARD, J.-Y. Une extension de l'interpretation de GSdel ~ l'analyse, et son application l'~limination des coupures dans l'analyse et la th~orie des types. In 2nd Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, Amsterdam, 1971, pp. 63-92.

Google Scholar

[22]

GIRARD, J.~Y. Interpretation fonctionelle et elimination des coupures de l'arithmetique d'ordre superieur. These D'Etat, Univ. Paris VII, Paris, 1972.

Google Scholar

[23]

GORDON, M. J., MILNER, R., AND WADSWORTH, C.P. Edinburgh Lecture Notes in Computer Science 78, Springer-Verlag, New York, 1979.

Google Scholar

[24]

GRi4TZER G. Universal Algebra. Van Nostrand, New York, 1968.

Google Scholar

[25]

GUTTAG, J. V., HOROWlTZ, E., AND MUSSER, D.R. Abstract data types and software validation. Commun. ACM 21, 12 (Dec. 1978), 1048-1064.

Crossref

Google Scholar

[26]

HAYNES, C.T. A theory of data type representation independence. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer- Verlag, New York, 1984, pp. 157-176.

Crossref

Google Scholar

[27]

HERRL1CH, H., AND STRECKER, G.E. Category Theory. Allyn and Bacon, Newton, Mass., 1973.

Google Scholar

[28]

HOOK, J.G. Understanding Russell--A first attempt. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 69-85.

Crossref

Google Scholar

[29]

HOOK, J., AND HOWE, D. Impredicative strong existential equivalent to type:type. Tech. Rep. TR 86-760, Cornell Univ., Ithaca, N.Y., 1986.

Crossref

Google Scholar

[30]

HOWARD, W. The formulas-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 479-490.

Google Scholar

[31]

HOWE, D.J. The computational behavior of Girard's paradox. In IEEE Symposium on Logic in Computer Science (June 1987). IEEE, New York, 1987, pp. 205-214.

Google Scholar

[32]

KAPUR, D. Towards a theory for abstract data types. Tech. Rep. MIT/LCS/TM-237, MIT, Cambridge, Mass., 1980.

Crossref

Google Scholar

[33]

KLEENE, S.C. Realizability: A retrospective survey. In Cambridge Summer School in Mathematical Logic. Lecture Notes in Mathematics 337, Springer-Verlag, New York, 1971, pp. 95-112.

Google Scholar

[34]

KRIPKE, S.A. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions. Proceedings of the 8th Logic Colloquium (Oxford, 1963). North-Holland, Amsterdam, 1965, pp. 92-130.

Google Scholar

[35]

LAMBEK, J. From lambda calculus to Cartesian closed categories. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Orlando, Fla., 1980, pp. 375-402.

Google Scholar

[36]

LANDIN, P.J. A correspondence between Algol 60 and Church's Lambda-notation. Commun.{ ACM 8, 2, 3 (Feb.-Mar. 1965), 89-101; 158-165.

Crossref

Google Scholar

[37]

LANDIN, P.J. The next 700 programming languages. Commun. ACM 9, 3 (Mar. 1966), 157-166.

Crossref

Google Scholar

[38]

L)/,UCHL1, H. Intuitionistic propositional calculus and definably non-empty terms. J. Symbolic Logic 30 (1965), 263.

Google Scholar

[39]

L~.UCHLI, H. An abstract notion of realizability for which intuitionistic predicate calculus is complete. In Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. (1968). North-Holland, Amsterdam, 1970, pp. 227-234.

Google Scholar

[40]

LEIVANT, D. Polymorphic type inference. In Proceedings of the lOth ACM Symposium on Principles of Programming Languages (Austin, Tex., Jan. 24-26, 1983). ACM, New York, 1983, pp. 88-98.

Crossref

Google Scholar

[41]

LISKOV, B., SNYDER, A., ATKINSON, R., AND SCHAFFERT, C. Abstraction mechanism in CLU. Commun. ACM 20, 8 (Aug. 1977), 564-576.

Crossref

Google Scholar

[42]

LISKOV, B. ET AL. CLU Reference Manual. Lecture Notes in Computer Science 114, Springer- Verlag, New York, 1981.

Crossref

Google Scholar

[43]

MAC LANE, S. Categories for the Working Mathematician. Graduate Texts in Mathematics 5, Springer-Verlag, New York, 1971.

Google Scholar

[44]

MACQUEEN, D.B. Modules for standard ML. In Polymorphism 2, 2 (1985), 35 pages. An earlier version appeared in Proceedings of 1984 ACM Symposium on Lisp and Functional Programming.

Crossref

Google Scholar

[45]

MACQUEEN, D.B. Using dependent types to express modular structure. In Proceedings of the 13th A CM Symposium on Principles of Programming Languages (St. Petersburg Beach, Flu, Jan. 13-15, 1986). ACM, New York, 1986, pp. 277-286.

Crossref

Google Scholar

[46]

MARTIN-LOF, P. Constructive mathematics and computer programming. Paper presented at The 6th International Congress for Logic, Methodology and Philosophy of Science. Preprint, Univ. of Stockholm, Dept. of Mathematics, Stockholm, 1979.

Google Scholar

[47]

MCCRACKEN, N. An investigation of a programming language with a polymorphic type structure. Ph.D. dissertation, Syracuse Univ., Syracuse, N.Y., 1979.

Crossref

Google Scholar

[48]

MCCRACKEN, N. The typechecking of programs with implicit type structure. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, 1984. Springer-Verlag, New York, pp. 301-316.

Crossref

Google Scholar

[49]

MEYER, A. R., AND REINHOLD, M. B. Type is not a type. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 13-15, 1986). ACM, New York, 1986. pp. 287-295.

Crossref

Google Scholar

[50]

MILNER, R. The standard ML core language. Polymorphism 2, 2 (1985), 28 pages. An earlier version appeared in Proceedings of 1984 ACM Symposium on Lisp and Functional Programming.

Google Scholar

[51]

MITCHELL, J. C. Semantic models for second-order Lambda calculus. In Proceedings of the 25th IEEE Symposium on Foundations of Computer Science (1984). IEEE, New York, 1984, pp. 289-299.

Google Scholar

[52]

MITCHELL, J. C. Representation independence and data abstraction. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages (St. Petersburg Beach, Fla., Jan. 13-15, 1986). ACM, New York, 1986, pp. 263-276.

Crossref

Google Scholar

[53]

MITCHELL, J.C. Polymo~phic type inference and containment. Inf. Comput. 76, 2/3 (Feb./Mar. 1988), 211-249.

Crossref

Google Scholar

[54]

MITCHELL, J. C., AND HARPER, R. The essence of ML. In Proceedings of the 15th ACM Symposium on Principles of Pragramming Languages (San Diego, Calif., Jan. 13-15, 1988). ACM, New York, 1988, pp. 28-46.

Crossref

Google Scholar

[55]

MITCHELL, J. C., AND MEYER, A. R. Second-order logical relations. In Logics of Programs. Lecture Notes in Computer Science 193, Springer-Verlag, New York, 1985, pp. 225-236.

Crossref

Google Scholar

[56]

MITCHELL, J. C., AND PLOTKIN, G.D. Abstract types have existential types. In Proceedings of the 12th ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan. 14-16, 1985). ACM, New York, 1985, pp. 37-51.

Crossref

Google Scholar

[57]

MITCHELL, J. G., MAYBERRY, W., AND SWEET, R. Mesa language manual. Tech. Rep. CSL- 79-3, Xerox PARC, Palo Alto, Calif., 1979.

Google Scholar

[58]

MORRIS, J. H. Types are not sets. In 1st ACM Symposium on Principles of Programming Languages (Boston, Mass., Oct. 1-3, 1973). ACM, New York, 1973, pp. 120-124.

Crossref

Google Scholar

[59]

O'DONNELL, M. A practical programming theorem which is independent of Peano arithmetic. In 11th ACM Symposium on the Theory of Computation (Atlanta, Ga., Apr. 30-May 2, 1979). ACM, New York, 1979, pp. 176-188.

Crossref

Google Scholar

[60]

PRAWlTZ, D. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.

Google Scholar

[61]

PRAWITZ, D. Ideas and results in proof theory. In 2nd Scandinavian Logic Symposium. North- Holland, Amsterdam, 1971, pp. 235-308.

Google Scholar

[62]

REYNOLDS, J.C. Towards a theory of type structure. In Paris Colloquium on Programming. Lecture Notes in Computer Science 19, Springer-Verlag, New York, 1974, pp. 408-425.

Crossref

Google Scholar

[63]

REYNOLDS, J.C. The essence of Algol. In Algorithmic Languages, J. W. de Bakker and J. C. van Vliet, Eds. IFIP, North-Holland, Amsterdam, 1981, pp. 345-372.

Google Scholar

[64]

REYNOLDS, J.C. Types, abstraction, and parametric polymorphism. In IFIP Congress (Paris, Sept. 1983).

Google Scholar

[65]

REYNOLDS, J.C. Polymorphism is not set-theoretic. In Proceedings of International Symposium on Semantics of Data Types. Lecture Notes in Computer Science 173, Springer-Verlag, New York, 1984, pp. 145-156.

Google Scholar

[66]

SHAW, M. (Ed.) ALPHARD: Form and Content. Springer-Verlag, New York, 1981.

Google Scholar

[67]

STATMAN, R. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9 (1979), 67-72.

Google Scholar

[68]

STATMAN, R. Number theoretic functions computable by polymorphic programs. In 22nd IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1981, pp. 279-282.

Google Scholar

[69]

STENLUND, S. Combinators, ),-terms and Proof Theory. Reidel, Dordrecht, Holland, 1972.

Google Scholar

[70]

TROELSTRA, A.S. Mathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer-Verlag, New York, 1973.

Google Scholar

[71]

WULF, W. W., LONDON, R., AND SHAW, M. An introduction to the construction and verification of Alphard programs. IEEE Trans. Softw. Eng. SE-2 (1976), 253-264.

Google Scholar

Cited By

View all

Racordon DFlesselle EBovel MErtl MKirsch C(2024)Existential Containers in ScalaProceedings of the 21st ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes10.1145/3679007.3685056(55-64)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679007.3685056
Fujita KSchubert AUrzyczyn PZdanowski K(2024)The existential fragment of second-order propositional intuitionistic logic is undecidableJournal of Applied Non-Classical Logics10.1080/11663081.2024.231277434:1(55-74)Online publication date: 6-Mar-2024
https://doi.org/10.1080/11663081.2024.2312774
Colaço JPauget BPouzet MHenriksen TSinkarovs A(2023)Polymorphic Types with Polynomial SizesProceedings of the 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming10.1145/3589246.3595372(36-49)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589246.3595372
Show More Cited By

Index Terms

Abstract types have existential type
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Polymorphic type inference and abstract data types
Polymorphic type inference and abstract data types

Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...

Reviews

Reviewer: David A. Watt

The title of this paper suggests a hot new discovery being rushed out of the laboratory and announced to the world. The reality is less exciting and says much about publication delays. The paper was first presented at a symposium in January 1985; it was submitted to TOPLAS in June 1986 and revised in March 1988. The delay should have provided an opportunity to polish the paper, but a number of careless errors have persisted, and the ML examples use syntax that is years out of date. The main theme of this paper is that existential types (which derive from constructive type theory) can be used to ascribe types to implementations of abstract types. For example, the omnipresent t-stack abstract type has the signature :.OC :.HB abstype tstack with empty: t-stack, push: t ? 9Tt-stack :2WZ t-stack, pop: t-stack :2WZ t ? 9Tt-stack :.HT :.OE and each of its implementations would have the existential type :.OC :.HB ? 9Ts. s ? 9T(t ? 9Ts :2WZ t)- ? 9T(s :2WZ t ? ).:.HT :.OE (the authors use ` ? for Cartesian product). Similarly, the t-queue abstract type might have the signature :.OC :.HB abstype t-queue with empty: t-queue insert: t ? 9Tt-queue:2WZ t-queue remove: t-queue :2WZ t ? t-queue, :.HT :.OE and the corresponding existential type would be :.OC :.HB ? Qq. q ? Q(t ? 9Tq :2WZ q)- ? q :2WZ t ? 9Tq).:.HT :.OE The above two existential types are equivalent; they are independent of the operations' names and of their intended semantics. Since abstract type implementations have types, they are first-class values and can be passed as parameters and returned as function results. The authors exploit these capabilities by presenting a tree-search function with a formal parameter of the above existential type. When the function is called with a stack implementation as an actual parameter, it performs a depth-first search. When called with a queue implementation, the function performs a breadth-first search (actually, right to left). This may not be useful in practice; the tree-search function is hard to understand. Another of the authors' examples is what must be the most opaque programming of the sieve algorithm ever published. This paper invites comparison with Cardelli and Wegner's 1985 survey paper on type theory [1]. The latter paper was more timely, more accurate, and more readable, yet it is not even referenced in this paper.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 10, Issue 3

July 1988

158 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/44501

Editor:
Susan L. Graham

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1988

Published in TOPLAS Volume 10, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

327
Total Citations
View Citations
2,526
Total Downloads

Downloads (Last 12 months)651
Downloads (Last 6 weeks)32

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Racordon DFlesselle EBovel MErtl MKirsch C(2024)Existential Containers in ScalaProceedings of the 21st ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes10.1145/3679007.3685056(55-64)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679007.3685056
Fujita KSchubert AUrzyczyn PZdanowski K(2024)The existential fragment of second-order propositional intuitionistic logic is undecidableJournal of Applied Non-Classical Logics10.1080/11663081.2024.231277434:1(55-74)Online publication date: 6-Mar-2024
https://doi.org/10.1080/11663081.2024.2312774
Colaço JPauget BPouzet MHenriksen TSinkarovs A(2023)Polymorphic Types with Polynomial SizesProceedings of the 9th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming10.1145/3589246.3595372(36-49)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3589246.3595372
SULZMANN MWEHR S(2023)A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic GoJournal of Functional Programming10.1017/S095679682300004733Online publication date: 9-Oct-2023
https://doi.org/10.1017/S0956796823000047
Rocha PCaires L(2023)Safe Session-Based Concurrency with Shared Linear StateProgramming Languages and Systems10.1007/978-3-031-30044-8_16(421-450)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_16
Zhuk DMartin B(2022)QCSP Monsters and the Demise of the Chen ConjectureJournal of the ACM10.1145/356382069:5(1-44)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3563820
Labrada EToro MTanter É(2022)Gradual System FJournal of the ACM10.1145/355598669:5(1-78)Online publication date: 28-Oct-2022
https://dl.acm.org/doi/10.1145/3555986
Appel APopescu AZdancewic S(2022)Coq’s vibrant ecosystem for verification engineering (invited talk)Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503951(2-11)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1145/3497775.3503951
Melicher DXu AZhao VPotanin AAldrich J(2022)Bounded Abstract EffectsACM Transactions on Programming Languages and Systems10.1145/349242744:1(1-48)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3492427
Lubbers M(2022)Deep Embedding with ClassTrends in Functional Programming10.1007/978-3-031-21314-4_3(39-58)Online publication date: 17-Mar-2022
https://dl.acm.org/doi/10.1007/978-3-031-21314-4_3
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.

Abstract

References

Cited By

Index Terms

Recommendations

Type checking and inference for polymorphic and existential types

Polymorphic type inference and abstract data types

Polymorphic type inference and abstract data types

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations