More Web Proxy on the site http://driver.im/

research-article

Open access

Internalizing representation independence with univalence

Authors:

Anders Mörtberg,

Max ZeunerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 12, Pages 1 - 30

https://doi.org/10.1145/3434293

Published: 04 January 2021 Publication History

Abstract

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations.

In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.

References

[1]

Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and Philip Wadler. 2020. Leibniz equality is isomorphic to Martin-Löf identity, parametricaJloluyr.nal of Functional Programming 30 ( 2020 ), e17. https://doi.org/10.1017/ S0956796820000155

[2]

Benedikt Ahrens and Peter LeFanu Lumsdaine. 2017. Displayed Categorie2sn.dInInternational Conference on Formal Structures for Computation and Deduction (FSCD 2017 ) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84 ), (Eds.). Springer International Publishing, Cham, 160-17h6t.tps://doi.org/10.1007/978-3-319-08970-6_11

[3]

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom2. 1Inst International Conference on Types for Proofs and Programs (TYPES 2015 ) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 69 ), Tarmo Uustalu (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 5 : 1-5 :34h.ttps://doi.org/10.4230/LIPIcs.TYPES. 2015.5

[4]

Cyril Cohen, Maxime Dénès, and Anders Mörtberg. 2013. Refinements for Free!. ICnertified Programs and Proofs (CPP 2013 ), Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing, Cham, 147-h1t6t2p. s://doi. org/10.1007/978-3-319-03545-1_10

[5]

hTierry Coquand and Nils Anders Danielsson. 2013. Isomorphism is equalityI. ndagationes Mathematicae 24, 4 ( 2013 ), 1105-1120. https://doi.org/10.1016/j.indag. 2013. 09. 00I2n memory of N.G. ( Dick) de Bruijn ( 1918-2012 ).

[6]

hTierry Coquand, Simon Huber, and Anders Mörtberg. 2018. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford, United Kingdom()LICS 2018 ). ACM, New York, NY, USA, 255-264. https://doi.org/10.1145/3209108.3209197

Digital Library

[7]

Karl Crary. 2017. Modules, Abstraction, and Parametric PolymorphisPmr. oIcneedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France)(POPL 2017 ). ACM, New York, NY, USA, 100-113. https://doi. org/10.1145/3009837.3009892

Digital Library

[8]

Nils Anders Danielsson. 2012. Bag Equivalence via a Proof-Relevant Membership RelatIinotne.raInctive Theorem Proving (Princeton, NJ, USA)( ITP 2012), Lennart Beringer and Amy Felty (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 149-165. https://doi.org/10.1007/978-3-642-32347-8_11

[9]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). InAutomated Deduction-CADE-25 (Berlin, Germany), Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378-38h8t.tps://doi.org/10.1007/978-3-319-21401-6_26

[10]

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. PIrnoceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India)(POPL 2015 ). Association for Computing Machinery, New York, NY, USA, 689-700. https://doi.org/10.1145/2676726.2677006

Digital Library

[11]

Edsger W. Dijkstra. 1974. On the role of scientific thought. (August 1974h)t.tps://www.cs.utexas.edu/users/EWD/ transcriptions/EWD04xx/EWD447.html

[12]

Martín Hötzel Escardó. 2019. Introduction to univalent foundations of mathematics wihtthtApsg:d//aw. ww.cs.bham.ac. uk/~mhe/ HoTT-UF-in-Agda-Lecture-Notes/index.html

[13]

Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani. 2020. Three Equivalent Ordinal Notation Systems in Cubical Agda. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) ( CPP 2020 ). Association for Computing Machinery, New York, NY, USA, 172-185h. ttps://doi.org/10.1145/ 3372885.3373835

[14]

Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide. 2018. Finite Sets in Homotopy Type Theory. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (Los Angeles, CA, USA) ( CPP 2018 ). Association for Computing Machinery, New York, NY, USA, 201-21h4.ttps://doi.org/10.1145/3167085

[15]

Emil Gjørup and Simon Friis Vindum. 2019. Case Study: BatchedQueue. https://github.com/limemloh/CubicalAgdaBatchedQueue

[16]

Håkon Robbestad Gylterud. 2020. Multisets in type thMeoartyh. ematical Proceedings of the Cambridge Philosophical Society 169, 1 ( 2020 ), 1-18. https://doi.org/10.1017/S0305004119000045

[17]

Florian Haftmann, Alexander Krauss, Ondřej Kunčar, and Tobias Nipkow. 2013. Data Refinement in Isabelle/HOL. In Interactive Theorem Proving (Rennes, France)(ITP 2013 ), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 100-115h.ttps://doi.org/10.1007/978-3-642-39634-2_10

[18]

Michael Hedberg. 1998. A coherence theorem for Martin-Löf's type thJeoourryn. al of Functional Programming 8, 4 ( 1998 ), 413-436. https://doi.org/10.1017/S0956796898003153

Digital Library

[19]

Stefan Kahrs, Donald Sannella, and Andrzej Tarlecki. 1997. The definition of Extended ML: A gentle introdTheuocrtetioicna. l Computer Science 173, 2 ( 1997 ), 445-484. https://doi.org/10.1016/S0304-3975 ( 96 ) 00163-6

Digital Library

[20]

Chris Kapulkin and Peter LeFanu Lumsdaine. 2020. The law of excluded middle in the simplicial model of type tThehoreyory. and Applications of Categories 35, 40 ( September 2020 ), 1546-1548. http://www.tac.mta.ca/tac/volumes/35/40/35-40.pdf

[21]

Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative S2o1rsttE. IAnCSL Annual Conference on Computer Science Logic (CSL 2012 ) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 16 ), Patrick Cégielski and Arnaud Durand (Eds.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 381-h3t9t5p.s://doi.org/10. 4230/LIPIcs.CSL. 2012.381

[22]

Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. 2017. Notions of Anonymous Existence in Martin-Löf Type Theory. Logical Methods in Computer Science 13, 1 ( 2017 ). https://doi.org/10.23638/LMCS-13 ( 1 :15) 2017

[23]

Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. ICnomputer Science Logic 2013 (CSL 2013 ) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 23 ), Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 432-451. https://doi.org/10.4230/LIPIcs.CSL. 2013.432

[24]

Peter Lammich. 2013. Automatic Data Refinement. IInnteractive Theorem Proving (Rennes, France)(ITP 2013 ), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 84-99. https://doi.org/10.1007/978-3-642-39634-2_9

Digital Library

[25]

Xavier Leroy. 1995. Applicative Functors and Fully Transparent Higher-Order ModulPeros. ceIendings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, California(P)OPL 1995 ). ACM, New York, NY, USA, 142-153. https://doi.org/10.1145/199448.199476

Digital Library

[26]

Dan Licata. 2016. Weak univalence with “beta” implies full univalence. https://groups.google.com/d/msg/ homotopytypetheory/j2KBIvDw53s/ YTDK4D0NFQAEJmail to Homotopy Type Theory mailing list.

[27]

Peter LeFanu Lumsdaine and Michael Shulman. 2019. Semantics of higher inductive tMyaptehse. matical Proceedings of the Cambridge Philosophical Society ( 2019 ). https://doi.org/10.1017/S030500411900015X

[28]

Nicolas Magaud. 2003. Changing Data Representation within the Coq SystTheeomre.mInProving in Higher Order Logics (Rome, Italy)( TPHOLs 2003 ), David Basin and Burkhart Wolf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 87-102. https://doi.org/10.1007/10930755_6

[29]

Nicolas Magaud and Yves Bertot. 2002. Changing Data Structures in Type Theory: A Study of Natural NumbTeyrps.esIn for Proofs and Programs (TYPES 2000 ) (Lecture Notes in Computer Science, Vol. 2277 ), Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 181-h1t9t6p.s://doi.org/10.1007/3-540-45842-5_12

[30]

Per Martin-Löf. 1975. An Intuitionistic Theory of Types: Predicative Part. LIongic Colloquium '73, H. E. Rose and J. C. Shepherdson (Eds.). Studies in Logic and the Foundations of Mathematics, Vol. 80. North-Hollandh, 7t3t-p1s1:/8/.doi. org/10.1016/ S0049-237X( 08 ) 71945-1

[31]

John C. Mitchell. 1986. Representation Independence and Data AbstractPioronc.eeIdnings of the 13th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages (St. Petersburg Beach, Florid(aP)OPL '86). Association for Computing Machinery, New York, NY, USA, 263-276.https://doi.org/10.1145/512644.512669

Digital Library

[32]

Andreas Nuyts and Dominique Devriese. 2018. Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. PIrnoceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Oxford, United Kingdom()LICS 2018 ). ACM, New York, NY, USA, 779-788. https://doi.org/10.1145/3209108.3209119

Digital Library

[33]

Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017. Parametric Quantifiers for Dependent Type Theory. Proceedings of the ACM on Programming Languages 1, ICFP, Article 32 ( January 2017 ), 29 pages.https://doi.org/10.1145/ 3110276

Digital Library

[34]

Chris Okasaki. 1999. Purely functional data structures. Cambridge University Press. https://doi.org/10.1017/ CBO9780511530104

[35]

John C. Reynolds. 1983. Types, Abstraction and Parametric PolymorphismIn. fIonrmation Processing '83: Proceedings of the IFIP 9th World Computer Congress, R. E. A. Mason (Ed.). North-Holland, 513-523.

[36]

Egbert Rijke. 2012. Homotopy Type Theory. Master's thesis. University of Ljubljanhat.tp://hottheory.files.wordpress.com/ 2012 /08/hott2.pdf

[37]

Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. 2019. Ornaments for Proof Reuse in1C0othq. InInternational Conference on Interactive Theorem Proving (ITP 2019 ) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 141 ), John Harrison, John O'Leary, and Andrew Tolmach (Eds.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 26 : 1-26 : 19. https://doi.org/10.4230/LIPIcs.ITP. 2019.26

[38]

Edmund Robinson. 1994. Parametricity as isomorphism. Theoretical Computer Science 136, 1 ( 1994 ), 163-181. https: //doi.org/10.1016/ 0304-3975 ( 94 ) 00126-4

Digital Library

[39]

Donald Sannella and Andrzej Tarlecki. 1987. On observational equivalence and algebraic specJific. aCtomiopnu. t. System Sci. 34, 2 ( 1987 ), 150-178. https://doi.org/10.1016/ 0022-0000 ( 87 ) 90023-7

Digital Library

[40]

hTomas Streicher. 1993. Investigations Into Intensional Type Theory. Habilitation thesis. Ludwig-Maximilians-Universität München. https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

[41]

Nicolas Tabareau, Éric Tanter, and Mathieu Sozeau. 2018. Equivalences for Free: Univalent Parametricity for Efective Transport. Proceedings of the ACM on Programming Languages 2, ICFP ( September 2018 ), 92 : 1-92 : 29. https://doi.org/ 10.1145/3236787

Digital Library

[42]

Nicolas Tabareau, Éric Tanter, and Mathieu Sozeau. 2019. The Marriage of Univalence and Parametricity. arXiv: 1909. 05027 [cs.PL] https://arxiv.org/abs/ 1909.05027Preprint.

[43]

hTe Agda Development Team. 2020. The Agda Programming Language. http://wiki.portal.chalmers.se/agda/pmwiki.php

[44]

hTe Coq Development Team. 2020. The Coq Proof Assistant. https://www.coq.inria.fr

[45]

hTe Mathematical Components Team. 2020. The Mathematical Components libraryh.ttps://github.com/math-comp/mathcomp

[46]

D. A. Turner. 1985. Miranda: A non-strict functional language with polymorphic tyFpuensc. tiIonnal Programming Languages and Computer Architecture (FPCA 1985 ), Jean-Pierre Jouannaud (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1-16.

[47]

hTe Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published. https://homotopytypetheory.org/book/

[48]

Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean.InInteractive Theorem Proving (Brasília, Brazil( ) ITP 2017 ), Mauricio Ayala-Rincón and César A. Muñoz (Eds.). Springer, Cham, 479-49h5.ttps: //doi.org/10.1007/978-3-319-66107-0_30

[49]

Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypePsr.oceedings of the ACM on Programming Languages 3, ICFP, Article 87 ( August 2019 ), 29 pages. https://doi.org/10.1145/3341691

Digital Library

[50]

Vladimir Voevodsky. 2010a. The equivalence axiom and univalent models of type theoryh. ttp://www.math.ias.edu/ vladimir/files/CMU_talk. pdNfotes from a talk at Carnegie Mellon University.

[51]

Vladimir Voevodsky. 2010b. Univalent Foundationhst.tps://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/ Bonn_talk. pdNfotes from a talk in Bonn.

[52]

Vladimir Voevodsky. 2015. An experimental library of formalized Mathematics based on the univalent fouMndaatht-ions. ematical Structures in Computer Science 25, 5 ( 2015 ), 1278-1294. https://doi.org/10.1017/S0960129514000577

[53]

Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. 2020. UniMath-a computer-checked library of univalent mathematics. https://github.com/UniMath/UniMath

[54]

Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (Imperial College, London, United Kingdo(mFP)CA ' 89 ). Association for Computing Machinery, New York, NY, USA, 347-359. https://doi.org/10.1145/99370.99404

Digital Library

[55]

James Wood. 2019. Vectors and Matrices in Agda. Blog poshttattps://personal.cis.strath.ac.uk/james.wood.100/blog/html/ VecMat.htm.l

Cited By

Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Cohen CCrance EMahboubi A(2024)Artifact Report: Trocq: Proof Transfer for Free, With or Without UnivalenceProgramming Languages and Systems10.1007/978-3-031-57262-3_11(269-274)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_11
Cohen CCrance EMahboubi A(2024)Trocq: Proof Transfer for Free, With or Without UnivalenceProgramming Languages and Systems10.1007/978-3-031-57262-3_10(239-268)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_10
Show More Cited By

Index Terms

Internalizing representation independence with univalence
1. Theory of computation
  1. Logic
    1. Type theory

Recommendations

Cubical agda: a dependently typed programming language with univalence and higher inductive types

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as ...
Trocq: Proof Transfer for Free, With or Without Univalence
Programming Languages and Systems
Abstract
This article presents Trocq, a new proof transfer framework for dependent type theory. Trocq is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding ...
Partial Univalence in n-truncated Type Theory
LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions.

A natural question is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
1,460
Total Downloads

Downloads (Last 12 months)324
Downloads (Last 6 weeks)64

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Van Muylder ANuyts ADevriese D(2024)Internal and Observational Parametricity for Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328508:POPL(209-240)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632850
Cohen CCrance EMahboubi A(2024)Artifact Report: Trocq: Proof Transfer for Free, With or Without UnivalenceProgramming Languages and Systems10.1007/978-3-031-57262-3_11(269-274)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_11
Cohen CCrance EMahboubi A(2024)Trocq: Proof Transfer for Free, With or Without UnivalenceProgramming Languages and Systems10.1007/978-3-031-57262-3_10(239-268)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_10
Dinges AHinze R(2023)What's in a Bag?: An “Application Proving Interface” for Finite Bags and its ImplementationProceedings of the 35th Symposium on Implementation and Application of Functional Languages10.1145/3652561.3652563(1-13)Online publication date: 29-Aug-2023
https://dl.acm.org/doi/10.1145/3652561.3652563
Lamiaux TLjungström AMörtberg AKrebbers RTraytel DPientka BZdancewic S(2023)Computing Cohomology Rings in Cubical AgdaProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575677(239-252)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575677
Kappelmann K(2023)Transport via Partial Galois Connections and EquivalencesProgramming Languages and Systems10.1007/978-981-99-8311-7_11(225-245)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_11
Kiiskinen S(2023)Curiously Empty Intersection of Proof Engineering and Computational SciencesImpact of Scientific Computing on Science and Society10.1007/978-3-031-29082-4_3(45-73)Online publication date: 8-Jul-2023
https://doi.org/10.1007/978-3-031-29082-4_3
Choudhury VKarwowski JSabry A(2022)Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languagesProceedings of the ACM on Programming Languages10.1145/34986676:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498667
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
Mörtberg A(2021)Cubical methods in homotopy type theory and univalent foundationsMathematical Structures in Computer Science10.1017/S096012952100031131:10(1147-1184)Online publication date: 10-Dec-2021
https://doi.org/10.1017/S0960129521000311

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents