{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:17:17Z","timestamp":1759637837439,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T00:00:00Z","timestamp":1599004800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003074","name":"Agencia Nacional de Promoci\u00f3n Cient\u00edfica y Tecnol\u00f3gica","doi-asserted-by":"publisher","award":["PICT 2019-1272"],"award-info":[{"award-number":["PICT 2019-1272"]}],"id":[{"id":"10.13039\/501100003074","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,2]]},"DOI":"10.1145\/3462172.3462198","type":"proceedings-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T22:06:52Z","timestamp":1627078012000},"page":"127-137","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Polymorphic System I"],"prefix":"10.1145","author":[{"given":"Cristian F.","family":"Sottile","sequence":"first","affiliation":[{"name":"Instituto de Investigaci\u00f3n en Ciencias de la Computaci\u00f3n (ICC). CONICET \/ Universidad de Buenos Aires., Buenos Aires, Argentina, Argentina"}]},{"given":"Alejandro","family":"D\u00edaz-Caro","sequence":"additional","affiliation":[{"name":"Dpto. de Ciencia y Tecnolog\u00eda., Universidad Nacional de Quilmes., Bernal, Buenos Aires, Argentina and Instituto de Investigaci\u00f3n en Ciencias, de la Computaci\u00f3n (ICC). CONICET \/ Universidad de Buenos Aires., Buenos Aires, Argentina"}]},{"given":"Pablo E.","family":"Mart\u00ednez L\u00f3pez","sequence":"additional","affiliation":[{"name":"Dpto. de Ciencia y Tecnolog\u00eda., Universidad Nacional de Quilmes., Bernal, Buenos Aires, Argentina"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A System F Accounting for Scalars. LMCS 8, 1:11","author":"Arrighi Pablo","year":"2012","unstructured":"Pablo Arrighi and Alejandro D\u00edaz-Caro . 2012. A System F Accounting for Scalars. LMCS 8, 1:11 ( 2012 ), 1\u201332. Pablo Arrighi and Alejandro D\u00edaz-Caro. 2012. A System F Accounting for Scalars. LMCS 8, 1:11 (2012), 1\u201332."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.04.001"},{"key":"e_1_3_2_1_3_1","first-page":"1","article-title":"Lineal: A linear-algebraic lambda-calculus","volume":"13","author":"Arrighi Pablo","year":"2017","unstructured":"Pablo Arrighi and Gilles Dowek . 2017 . Lineal: A linear-algebraic lambda-calculus . LMCS 13 , 1:8 (2017), 1 \u2013 33 . Pablo Arrighi and Gilles Dowek. 2017. Lineal: A linear-algebraic lambda-calculus. LMCS 13, 1:8 (2017), 1\u201333.","journal-title":"LMCS"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1003"},{"key":"e_1_3_2_1_5_1","first-page":"918","article-title":"A Relational Semantics for Parallelism and Non-Determinism in a Functional Setting","volume":"163","author":"Bucciarelli Antonio","year":"2012","unstructured":"Antonio Bucciarelli , Thomas Ehrhard , and Giulio Manzonetto . 2012 . A Relational Semantics for Parallelism and Non-Determinism in a Functional Setting . APAL 163 , 7 (2012), 918 \u2013 934 . Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. 2012. A Relational Semantics for Parallelism and Non-Determinism in a Functional Setting. APAL 163, 7 (2012), 918\u2013934.","journal-title":"APAL"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1145"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794275860"},{"volume-title":"Isomorphisms of types: from \u03bb-calculus to information retrieval and language design","author":"Cosmo Roberto Di","key":"e_1_3_2_1_9_1","unstructured":"Roberto Di Cosmo . 1995. Isomorphisms of types: from \u03bb-calculus to information retrieval and language design . Birkhauser , Switzerland . Roberto Di Cosmo. 1995. Isomorphisms of types: from \u03bb-calculus to information retrieval and language design. Birkhauser, Switzerland."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Alejandro D\u00edaz-Caro and Gilles Dowek. 2013. Non determinism through type isomorphism. EPTCS (LSFA\u201912) 113(2013) 137\u2013144.  Alejandro D\u00edaz-Caro and Gilles Dowek. 2013. Non determinism through type isomorphism. EPTCS (LSFA\u201912) 113(2013) 137\u2013144.","DOI":"10.4204\/EPTCS.113.13"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Alejandro D\u00edaz-Caro and Gilles Dowek. 2017. Typing quantum superpositions and measurement. LNCS (TPNC\u201917) 10687(2017) 281\u2013293.  Alejandro D\u00edaz-Caro and Gilles Dowek. 2017. Typing quantum superpositions and measurement. LNCS (TPNC\u201917) 10687(2017) 281\u2013293.","DOI":"10.1007\/978-3-319-71069-3_22"},{"key":"e_1_3_2_1_12_1","unstructured":"Alejandro D\u00edaz-Caro and Gilles Dowek. 2019. Proof Normalisation in a Logic Identifying Isomorphic Propositions. LIPIcs (FSCD\u201919) 131(2019) 14:1\u201314:23.  Alejandro D\u00edaz-Caro and Gilles Dowek. 2019. Proof Normalisation in a Logic Identifying Isomorphic Propositions. LIPIcs (FSCD\u201919) 131(2019) 14:1\u201314:23."},{"key":"e_1_3_2_1_13_1","unstructured":"Alejandro D\u00edaz-Caro and Gilles Dowek. 2020. Extensional proofs in a propositional logic modulo isomorphisms. arXiv:2002.03762.  Alejandro D\u00edaz-Caro and Gilles Dowek. 2020. Extensional proofs in a propositional logic modulo isomorphisms. arXiv:2002.03762."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3470152.3470208"},{"key":"e_1_3_2_1_15_1","first-page":"1","article-title":"Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of \u03bb+","volume":"2015","author":"D\u00edaz-Caro Alejandro","year":"2015","unstructured":"Alejandro D\u00edaz-Caro and Pablo\u00a0 E. Mart\u00ednez\u00a0L\u00f3pez . 2015 . Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of \u03bb+ . ACM IFL 2015 , 9 (2015), 1 \u2013 11 . Alejandro D\u00edaz-Caro and Pablo\u00a0E. Mart\u00ednez\u00a0L\u00f3pez. 2015. Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of \u03bb+. ACM IFL 2015, 9 (2015), 1\u201311.","journal-title":"ACM IFL"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027357912519"},{"key":"e_1_3_2_1_17_1","first-page":"1289","article-title":"Proof normalization modulo","volume":"68","author":"Dowek Gilles","year":"2003","unstructured":"Gilles Dowek and Benjamin Werner . 2003 . Proof normalization modulo . JSL 68 , 4 (2003), 1289 \u2013 1316 . Gilles Dowek and Benjamin Werner. 2003. Proof normalization modulo. JSL 68, 4 (2003), 1289\u20131316.","journal-title":"JSL"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.174434"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.34.6"},{"volume-title":"Proofs and types","author":"Girard Jean-Yves","key":"e_1_3_2_1_20_1","unstructured":"Jean-Yves Girard , Paul Taylor , and Yves Lafont . 1989. Proofs and types . Cambridge U.P. , UK. Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Cambridge U.P., UK."},{"key":"e_1_3_2_1_21_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Bibliopolis Napoli Italy.  Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Bibliopolis Napoli Italy."},{"key":"e_1_3_2_1_22_1","first-page":"1","article-title":"Linearity, non-determinism and solvability","volume":"103","author":"Pagani Michele","year":"2010","unstructured":"Michele Pagani and Simona Ronchi Della Rocca . 2010 . Linearity, non-determinism and solvability . Fund. Inf. 103 , 1 \u2013 4 (2010), 173\u2013202. Michele Pagani and Simona Ronchi Della Rocca. 2010. Linearity, non-determinism and solvability. Fund. Inf. 103, 1\u20134 (2010), 173\u2013202.","journal-title":"Fund. Inf."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9287-4"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_117"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Cristian\u00a0F. Sottile Alejandro D\u00edaz-Caro and Pablo\u00a0E. Mart\u00ednez\u00a0L\u00f3pez. 2021. Polymorphic System I. arXiv:2101.03215.  Cristian\u00a0F. Sottile Alejandro D\u00edaz-Caro and Pablo\u00a0E. Mart\u00ednez\u00a0L\u00f3pez. 2021. Polymorphic System I. arXiv:2101.03215.","DOI":"10.1145\/3462172.3462198"},{"volume-title":"HoTT: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","key":"e_1_3_2_1_26_1","unstructured":"The Univalent Foundations Program . 2013. HoTT: Univalent Foundations of Mathematics . Institute for Advanced Study , Princeton, NJ, USA . The Univalent Foundations Program. 2013. HoTT: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ, USA."},{"key":"e_1_3_2_1_27_1","first-page":"1029","article-title":"The algebraic lambda calculus","volume":"19","author":"Vaux Lionel","year":"2009","unstructured":"Lionel Vaux . 2009 . The algebraic lambda calculus . MSCS 19 , 5 (2009), 1029 \u2013 1059 . Lionel Vaux. 2009. The algebraic lambda calculus. MSCS 19, 5 (2009), 1029\u20131059.","journal-title":"MSCS"}],"event":{"name":"IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages","acronym":"IFL 2020","location":"Canterbury United Kingdom"},"container-title":["Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462198","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462172.3462198","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:34Z","timestamp":1750191454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462198"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,2]]},"references-count":27,"alternative-id":["10.1145\/3462172.3462198","10.1145\/3462172"],"URL":"https:\/\/doi.org\/10.1145\/3462172.3462198","relation":{},"subject":[],"published":{"date-parts":[[2020,9,2]]},"assertion":[{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}