{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:49Z","timestamp":1772164009455,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M016951\/1"],"award-info":[{"award-number":["EP\/M016951\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837638","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"18-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["Type theory in type theory using quotient inductive types"],"prefix":"10.1145","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[{"name":"University of Nottingham, UK"}]},{"given":"Ambrus","family":"Kaposi","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"nlab: Beck-chevalley condition. Available online. Accessed: 2015-10- 26.  nlab: Beck-chevalley condition. Available online. Accessed: 2015-10- 26."},{"key":"e_1_3_2_1_2_1","unstructured":"The Agda Wiki 2015. Available online.  The Agda Wiki 2015. Available online."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"T. Altenkirch and A. Kaposi. Supplementary material for the paper Type Theory in Type Theory using Quotient Inductive Types 2015. Available online at the second author\u2019s website.  T. Altenkirch and A. Kaposi. Supplementary material for the paper Type Theory in Type Theory using Quotient Inductive Types 2015. Available online at the second author\u2019s website.","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"T. Altenkirch M. Hofmann and T. Streicher. Categorical reconstruction of a reduction free normalization proof. In D. Pitt D. E. Rydeheard and P. Johnstone editors Category Theory and Computer Science LNCS 953 pages 182\u2013199 1995.   T. Altenkirch M. Hofmann and T. Streicher. Categorical reconstruction of a reduction free normalization proof. In D. Pitt D. E. Rydeheard and P. Johnstone editors Category Theory and Computer Science LNCS 953 pages 182\u2013199 1995.","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2040096.2040104"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_8_1","first-page":"128","volume-title":"19th International Conference on Types for Proofs and Programs (TYPES 2013","volume":"26","author":"Bezem M.","year":"2014"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676988"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_1_13_1","unstructured":"N.\n       \n      Danielsson\n    .\n      \n  \n   \n  A formalisation of a dependently typed language as an inductive-recursive family. In T. Altenkirch and C. McBride editors Types for Proofs and Programs volume \n  4502\n   of \n  Lecture Notes in Computer Science pages 93\u2013\n  109\n  . Springer Berlin Heidelberg 2007. ISBN 978-3-540-74463-4.   N. Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In T. Altenkirch and C. McBride editors Types for Proofs and Programs volume 4502 of Lecture Notes in Computer Science pages 93\u2013109. Springer Berlin Heidelberg 2007. ISBN 978-3-540-74463-4."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500575"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1975-0373893-X"},{"key":"e_1_3_2_1_16_1","first-page":"134","volume-title":"Types for Proofs and Programs","author":"Dybjer P."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003153"},{"key":"e_1_3_2_1_18_1","volume-title":"Department of Computer Science","author":"Hofmann M.","year":"1995"},{"key":"e_1_3_2_1_19_1","first-page":"54","volume-title":"Extensional Constructs in Intensional Type Theory","author":"Hofmann M."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.49"},{"key":"e_1_3_2_1_21_1","volume-title":"University of Nottingham","author":"Kraus N.","year":"2015"},{"key":"e_1_3_2_1_22_1","unstructured":"D. Licata. Running circles around (in) your proof assistant; or quotients that compute 2011. Available online.  D. Licata. Running circles around (in) your proof assistant; or quotients that compute 2011. Available online."},{"key":"e_1_3_2_1_23_1","volume-title":"University of Edinburgh","author":"McBride C.","year":"1999"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_3_2_1_25_1","first-page":"361","volume-title":"Proceedings of the Logical Frameworks Workshop","author":"Mendler N.","year":"1990"},{"key":"e_1_3_2_1_26_1","volume-title":"Swansea University","author":"Forsberg F. Nordvall","year":"2013"},{"key":"e_1_3_2_1_27_1","volume-title":"Chalmers University of Technology","author":"Norell U.","year":"2007"},{"key":"e_1_3_2_1_28_1","unstructured":"F. Pfenning. Church and curry: Combining intrinsic and extrinsic typing. 2008.  F. Pfenning. Church and curry: Combining intrinsic and extrinsic typing. 2008."},{"key":"e_1_3_2_1_29_1","unstructured":"A. Pitts. Quotient types in Agda. Private email May 2015.  A. Pitts. Quotient types in Agda. Private email May 2015."},{"key":"e_1_3_2_1_30_1","first-page":"523","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds J. C."},{"key":"e_1_3_2_1_31_1","volume-title":"Institute for Advanced Study","author":"Foundations Program The Univalent","year":"2013"},{"key":"e_1_3_2_1_32_1","unstructured":"V. Voevodsky. A type system with two kinds of identity types. Slides of a talk at the Institute for Advanced Study February 2013.  V. Voevodsky. A type system with two kinds of identity types. Slides of a talk at the Institute for Advanced Study February 2013."}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:37Z","timestamp":1750211017000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":32,"alternative-id":["10.1145\/2837614.2837638","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837638","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837638","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}