{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:28Z","timestamp":1772164048198,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"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,9,25]]},"DOI":"10.1145\/2500365.2500577","type":"proceedings-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T09:13:17Z","timestamp":1380100397000},"page":"61-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Type-theory in color"],"prefix":"10.1145","author":[{"given":"Jean-Philippe","family":"Bernardy","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]},{"given":"Moulin","family":"Guilhem","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2013,9,25]]},"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.2168\/LMCS-8(1:29)2012"},{"key":"e_1_3_2_2_3_1","volume-title":"Lambda calculi with types. Handbook of logic in computer science, 2:117--309","author":"Barendregt H. P.","year":"1992","unstructured":"H. P. Barendregt . Lambda calculi with types. Handbook of logic in computer science, 2:117--309 , 1992 . H. P. Barendregt. Lambda calculi with types. Handbook of logic in computer science, 2:117--309, 1992."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"J.-P.\n      Bernardy\n     and \n      M.\n      Lasson\n  . \n  Realizability and parametricity in pure type systems\n  . In M. Hofmann editor FoSSaCS volume \n  6604\n   of \n  LNCS pages \n  108\n  --\n  122\n  . \n  Springer 2011\n  .   J.-P. Bernardy and M. Lasson. Realizability and parametricity in pure type systems. In M. Hofmann editor FoSSaCS volume 6604 of LNCS pages 108--122. Springer 2011.","DOI":"10.1007\/978-3-642-19805-2_8"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.25"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_2_8_1","volume-title":"INRIA","author":"Coquand T.","year":"1986","unstructured":"T. Coquand and G. Huet . The calculus of constructions. Technical report , INRIA , 1986 . T. Coquand and G. Huet. The calculus of constructions. Technical report, INRIA, 1986."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364544"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103697"},{"key":"e_1_3_2_2_11_1","volume-title":"Bibliopolis","author":"Martin-Lof P.","year":"1984","unstructured":"P. Martin-Lof . Intuitionistic type theory . Bibliopolis , 1984 . P. Martin-Lof. Intuitionistic type theory. Bibliopolis, 1984."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792828"},{"key":"e_1_3_2_2_13_1","volume-title":"Chalmers Tekniska Hogskola","author":"Norell U.","year":"2007","unstructured":"U. Norell . Towards a practical programming language based on dependent type theory. PhD thesis , Chalmers Tekniska Hogskola , 2007 . URL http:\/\/publications.lib.chalmers.se\/cpl\/record\/index.xsql?pubid=46311. U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers Tekniska Hogskola, 2007. URL http:\/\/publications.lib.chalmers.se\/cpl\/record\/index.xsql?pubid=46311."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_3_2_2_16_1","volume-title":"Ecole Polytechnique","author":"Siles V.","year":"2010","unstructured":"V. Siles . Investigation on the typing of equality in type systems. Phd thesis , Ecole Polytechnique , 2010 . V. Siles. Investigation on the typing of equality in type systems. Phd thesis, Ecole Polytechnique, 2010."},{"key":"e_1_3_2_2_17_1","volume-title":"The Coq proof assistant","author":"The Coq","year":"2012","unstructured":"The Coq development team. The Coq proof assistant , 2012 . URL http:\/\/coq.inria.fr. The Coq development team. The Coq proof assistant, 2012. URL http:\/\/coq.inria.fr."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.042"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","location":"Boston Massachusetts USA","acronym":"ICFP'13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","Northeastern University"]},"container-title":["Proceedings of the 18th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500577","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2500365.2500577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:32Z","timestamp":1750217672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,25]]},"references-count":20,"alternative-id":["10.1145\/2500365.2500577","10.1145\/2500365"],"URL":"https:\/\/doi.org\/10.1145\/2500365.2500577","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2544174.2500577","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,9,25]]},"assertion":[{"value":"2013-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}