{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:23Z","timestamp":1772164043027,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429082","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"87-100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Abstraction and invariance for algebraically indexed types"],"prefix":"10.1145","author":[{"given":"Robert","family":"Atkey","sequence":"first","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Kennedy","sequence":"additional","affiliation":[{"name":"Microsoft Research Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_5"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_7"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_2_6_1","first-page":"78","volume-title":"Programs","author":"Cardelli L.","year":"2010","unstructured":"L. Cardelli , P. Gardner . Processes in Space . Programs , Proofs, Processes : Proceedings, CiE , pp. 78 -- 87 , %LNCS vol. 6158 , 2010 . L. Cardelli, P. Gardner.Processes in Space. Programs, Proofs, Processes: Proceedings, CiE, pp. 78--87, %LNCS vol. 6158, 2010."},{"key":"e_1_3_2_2_7_1","unstructured":"Computational Geometry Algorithms Library (CGAL): User and ReferenceManual. Available at http:\/\/www.cgal.org.  Computational Geometry Algorithms Library (CGAL): User and ReferenceManual. Available at http:\/\/www.cgal.org."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-9961-0","volume-title":"Geometric Methods and Applications For ComputerScience and Engineering","author":"Gallier J.","year":"2011","unstructured":"J. Gallier . Geometric Methods and Applications For ComputerScience and Engineering . Springer , 2011 . J. Gallier. Geometric Methods and Applications For ComputerScience and Engineering. Springer, 2011."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_3"},{"key":"e_1_3_2_2_11_1","first-page":"149","volume-title":"Formal Logical Methods for System Security andCorrectness","author":"Hofmann M.","year":"2008","unstructured":"M. Hofmann . Correctness of Effect-based ProgramTransformations . Formal Logical Methods for System Security andCorrectness , pp. 149 -- 173 , 2008 . M. Hofmann. Correctness of Effect-based ProgramTransformations. Formal Logical Methods for System Security andCorrectness, pp. 149--173, 2008."},{"key":"e_1_3_2_2_12_1","first-page":"97","volume-title":"Proceedings, AFP","author":"Jones M. P.","year":"1995","unstructured":"M. P. Jones . Functional Programming with Overloading and Higher-OrderPolymorphism . Proceedings, AFP ,pp. 97 -- 136 , 1995 . M. P. Jones. Functional Programming with Overloading and Higher-OrderPolymorphism. Proceedings, AFP,pp. 97--136, 1995."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263761"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/978-3-642-17685-2_8","volume-title":"Types for Units-of-Measure: Theory and Practice.Central European Functional Programming school (CEFP)","author":"Kennedy A. J.","year":"2010","unstructured":"A. J. Kennedy . Types for Units-of-Measure: Theory and Practice.Central European Functional Programming school (CEFP) , pp. 268 -- 305 , LNCS vol. 6299, 2010 . A. J. Kennedy. Types for Units-of-Measure: Theory and Practice.Central European Functional Programming school (CEFP), pp. 268--305, LNCS vol. 6299, 2010."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_2_18_1","first-page":"513","volume":"83","author":"Reynolds J. C.","year":"1983","unstructured":"J. C. Reynolds . Types, Abstraction and Parametric Polymorphism . Information Processing 83 , pp. 513 -- 523 , 1983 . J. C. Reynolds. Types, Abstraction and Parametric Polymorphism. Information Processing 83, pp. 513--523, 1983.","journal-title":"Information Processing"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011553200337"},{"key":"e_1_3_2_2_20_1","volume-title":"Proving Noninterference by a FullyComplete Translation to the Simply Typed lambda-calculus. Logical Methods in Computer Science 4(3)","author":"Shikuma N.","year":"2008","unstructured":"N. Shikuma and A. Igarahsi . Proving Noninterference by a FullyComplete Translation to the Simply Typed lambda-calculus. Logical Methods in Computer Science 4(3) , 2008 . N. Shikuma and A.Igarahsi. Proving Noninterference by a FullyComplete Translation to the Simply Typed lambda-calculus. Logical Methods in Computer Science 4(3), 2008."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016868"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429082","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429082","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":21,"alternative-id":["10.1145\/2429069.2429082","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429082","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429082","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}