{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:43:23Z","timestamp":1743151403562,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031169113"},{"type":"electronic","value":"9783031169120"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-16912-0_2","type":"book-chapter","created":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T07:04:02Z","timestamp":1663743842000},"page":"34-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Subtyping Without Reduction"],"prefix":"10.1007","author":[{"given":"Brandon","family":"Hewer","sequence":"first","affiliation":[]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,22]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Ghani, N., Hancock, P., McBride, C., Morris, P.: Indexed containers. J. Funct. Program. 25 (2015)","key":"2_CR1","DOI":"10.1017\/S095679681500009X"},{"doi-asserted-by":"crossref","unstructured":"Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 257\u2013268 (2014)","key":"2_CR2","DOI":"10.1145\/2628136.2628139"},{"unstructured":"Cohen, C., Coquand, T., Huber, S., M\u00f6rtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. arXiv preprint arXiv:1611.02108 (2016)","key":"2_CR3"},{"doi-asserted-by":"crossref","unstructured":"Dybjer, P., Setzer, A.: Induction-recursion and initial algebras. Ann. Pure Appl. Log. 124(1\u20133) (2003)","key":"2_CR4","DOI":"10.1016\/S0168-0072(02)00096-9"},{"doi-asserted-by":"publisher","unstructured":"Gilbert, G., Cockx, J., Sozeau, M., Tabareau, N.: Definitional proof-irrelevance without K. Proc. ACM Program. Lang. 3(POPL) (Jan 2019). https:\/\/doi.org\/10.1145\/3290316","key":"2_CR5","DOI":"10.1145\/3290316"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-38946-7_13","volume-title":"Typed Lambda Calculi and Applications","author":"P Hancock","year":"2013","unstructured":"Hancock, P., McBride, C., Ghani, N., Malatesta, L., Altenkirch, T.: Small induction recursion. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 156\u2013172. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38946-7_13"},{"unstructured":"Hewer, B.: Subtyping Cubical Agda Library (2022). https:\/\/tinyurl.com\/f8pezwxd","key":"2_CR7"},{"unstructured":"Kraus, N.: Ph.D. thesis, University of Nottingham (2015)","key":"2_CR8"},{"unstructured":"Malatesta, L., Altenkirch, T., Ghani, N., Hancock, P., McBride, C.: Small induction recursion, indexed containers and dependent polynomials are equivalent (2012)","key":"2_CR9"},{"doi-asserted-by":"crossref","unstructured":"Morris, P., Altenkirch, T.: Indexed containers. In: IEEE Symposium in Logic in Computer Science (2009)","key":"2_CR10","DOI":"10.1109\/LICS.2009.33"},{"unstructured":"Shulman, M.: Higher inductive-recursive univalence and type-directed definitions, June 2014. https:\/\/homotopytypetheory.org\/2014\/06\/08\/hiru-tdd\/","key":"2_CR11"},{"unstructured":"Program, T.U.F.: Homotopy type theory: univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)","key":"2_CR12"},{"doi-asserted-by":"crossref","unstructured":"Vezzosi, A., M\u00f6rtberg, A., Abel, A.: Cubical Agda: a dependently typed programming language with univalence and higher inductive types. J. Funct. Program. 31 (2021)","key":"2_CR13","DOI":"10.1017\/S0956796821000034"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-16912-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T23:36:22Z","timestamp":1663803382000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-16912-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031169113","9783031169120"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-16912-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"22 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tblilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mpc2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.macs.hw.ac.uk\/mpc22\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 invited talks (given as abstracts in preface)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}