{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T22:00:31Z","timestamp":1775944831493,"version":"3.50.1"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030521998","type":"print"},{"value":"9783030522001","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-52200-1_25","type":"book-chapter","created":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T18:04:48Z","timestamp":1594145088000},"page":"253-259","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Equality Checking for General Type Theories in Andromeda 2"],"prefix":"10.1007","author":[{"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"given":"Philipp G.","family":"Haselwarter","sequence":"additional","affiliation":[]},{"given":"Anja","family":"Petkovi\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. In: Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, December 2017","DOI":"10.1145\/3158111"},{"key":"25_CR2","unstructured":"Abel, A., Scherer, G.: On irrelevance and algorithmic equality in predicative type theory. Log. Methods Comput. Sci. 8(1) (2012). \nhttps:\/\/lmcs.episciences.org\/1045"},{"key":"25_CR3","unstructured":"The Agda proof assistant. \nhttps:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"25_CR4","unstructured":"The Andromeda proof assistant. \nhttp:\/\/www.andromeda-prover.org\/"},{"key":"25_CR5","unstructured":"Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the Andromeda proof assistant. In: 22nd International Conference on Types for Proofs and Programs (TYPES 2016). LIPIcs, vol. 97, pp. 5:1\u20135:31 (2018)"},{"key":"25_CR6","unstructured":"Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: 22nd International Conference on Types for Proofs and Programs TYPES 2016. University of Novi Sad (2016)"},{"key":"25_CR7","unstructured":"The Coq proof assistant. \nhttps:\/\/coq.inria.fr\/"},{"key":"25_CR8","unstructured":"The Dedukti logical framework. \nhttps:\/\/deducteam.github.io"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Gilbert, G., Cockx, J., Sozeau, M., Tabareau, N.: Definitional proof-irrelevance without $$K$$. In: Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, January 2019","DOI":"10.1145\/3290316"},{"key":"25_CR10","unstructured":"The MMT language and system. \nhttps:\/\/uniformal.github.io\/\/"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"issue":"4","key":"25_CR12","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/3234693","volume":"19","author":"F Rabe","year":"2018","unstructured":"Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 24:1\u201324:43 (2018)","journal-title":"ACM Trans. Comput. Log."},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. In: Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, December 2019","DOI":"10.1145\/3371076"},{"issue":"4","key":"25_CR14","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1145\/1183278.1183281","volume":"7","author":"CA Stone","year":"2006","unstructured":"Stone, C.A., Harper, R.: Extensional equivalence and singleton types. ACM Trans. Comput. Log. 7(4), 676\u2013722 (2006)","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2020"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-52200-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T19:07:19Z","timestamp":1594148839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-52200-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030521998","9783030522001"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-52200-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"8 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICMS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Congress on Mathematical Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Braunschweig","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icms2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.iaa.tu-bs.de\/AppliedAlgebra\/ICMS2020\/ICMS2020.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"58","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":"48","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":"83% - 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":"2.22","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":"3.67","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","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)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}