{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:54:54Z","timestamp":1770278094655,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"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":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209119","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"779-788","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Degrees of Relatedness"],"prefix":"10.1145","author":[{"given":"Andreas","family":"Nuyts","sequence":"first","affiliation":[{"name":"imec-DistriNet, KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"imec-DistriNet, KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_2_1","first-page":"797","article-title":"Polarised subtyping for sized types","volume":"18","author":"Abel Andreas","year":"2008","unstructured":"Andreas Abel . 2008 . Polarised subtyping for sized types . MSCS 18 , 5 (2008), 797 -- 822 . Andreas Abel. 2008. Polarised subtyping for sized types. MSCS 18, 5 (2008), 797--822.","journal-title":"MSCS"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.006"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_10_1","volume-title":"Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In TYPES '15","author":"Cohen Cyril","year":"2015","unstructured":"Cyril Cohen , Thierry Coquand , Simon Huber , and Anders M\u00f6rtberg . 2015 . Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In TYPES '15 . Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2015. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In TYPES '15."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_11"},{"key":"e_1_3_2_1_12_1","first-page":"13","article-title":"Syntax and semantics of dependent types. Springer London, London","volume":"4","author":"Hofmann Martin","year":"1997","unstructured":"Martin Hofmann . 1997 . Syntax and semantics of dependent types. Springer London, London , Chapter 4 , 13 -- 54 . Martin Hofmann. 1997. Syntax and semantics of dependent types. Springer London, London, Chapter 4, 13--54.","journal-title":"Chapter"},{"key":"e_1_3_2_1_13_1","unstructured":"Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Unpublished note. (1997).  Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. Unpublished note. (1997)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_1_15_1","volume-title":"Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In CSL 2013 (LIPIcs)","volume":"23","author":"Neelakantan","unstructured":"Neelakantan R. Krishnaswami and Derek Dreyer. 2013 . Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In CSL 2013 (LIPIcs) , Vol. 23 . Dagstuhl, Germany, 432--451. Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In CSL 2013 (LIPIcs), Vol. 23. Dagstuhl, Germany, 432--451."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90053-5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_2_1_18_1","volume-title":"Internal Universes in Models of Homotopy Type Theory. In FSCD '18","author":"Licata Daniel R.","year":"2018","unstructured":"Daniel R. Licata , Ian Orton , Andrew M. Pitts , and Bas Spitters . 2018 . Internal Universes in Models of Homotopy Type Theory. In FSCD '18 . Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In FSCD '18."},{"key":"e_1_3_2_1_19_1","volume-title":"LFCS '16","author":"Daniel","unstructured":"Daniel R. Licata and Michael Shulman. 2016. Adjoint Logic with a 2-Category of Modes . In LFCS '16 . Daniel R. Licata and Michael Shulman. 2016. Adjoint Logic with a 2-Category of Modes. In LFCS '16."},{"key":"e_1_3_2_1_20_1","volume-title":"FSCD '17","author":"Licata Daniel R.","year":"2017","unstructured":"Daniel R. Licata , Michael Shulman , and Mitchell Riley . 2017 . A Fibrational Framework for Substructural and Modal Logics . In FSCD '17 . 25:1--25:22. Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017. A Fibrational Framework for Substructural and Modal Logics. In FSCD '17. 25:1--25:22."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.03.005"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In TLCA. 344--359.   Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In TLCA. 344--359.","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. 350--364.  Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. 350--364.","DOI":"10.1007\/978-3-540-78499-9_25"},{"key":"e_1_3_2_1_24_1","unstructured":"Guilhem Moulin. 2016. Internalizing Parametricity. Ph.D. Dissertation. Chalmers University of Technology Sweden.  Guilhem Moulin. 2016. Internalizing Parametricity. Ph.D. Dissertation. Chalmers University of Technology Sweden."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_16"},{"key":"e_1_3_2_1_30_1","volume-title":"IFIP Congress. 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds . 1983 . Types, Abstraction and Parametric Polymorphism .. In IFIP Congress. 513--523 . John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism.. In IFIP Congress. 513--523."},{"key":"e_1_3_2_1_32_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book IAS.  The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book IAS."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Oxford United Kingdom","acronym":"LICS '18","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209119","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:07Z","timestamp":1750212427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209119"}},"subtitle":["A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory"],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":30,"alternative-id":["10.1145\/3209108.3209119","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209119","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}