{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:02:26Z","timestamp":1743062546541,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572616"},{"type":"electronic","value":"9783031572623"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>Trocq<\/jats:sc>\u00a0[5] is both the name of a calculus, describing a parametricity framework, and of a  plugin\u00a0[6] that provides tactics for performing representation changes in goals, as well as vernacular commands for specifying the expected translations.<\/jats:p>","DOI":"10.1007\/978-3-031-57262-3_11","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"269-274","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence"],"prefix":"10.1007","author":[{"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enzo","family":"Crance","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"11_CR1","unstructured":"Anand, A., Morrisett, G.: Revisiting parametricity: Inductives and uniformity of propositions (2017), http:\/\/arxiv.org\/abs\/1705.01163"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Angiuli, C., Cavallo, E., M\u00f6rtberg, A., Zeuner, M.: Internalizing representation independence with univalence. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021)","DOI":"10.1145\/3434293"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Pons, O.: Type isomorphisms and proof reuse in dependent type theory. In: FoSSaCS. LNCS, vol.\u00a02030, pp. 57\u201371. Springer (2001)","DOI":"10.1007\/3-540-45315-6_4"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Blot, V., Cousineau, D., Crance, E., de\u00a0Prisque, L.D., Keller, C., Mahboubi, A., Vial, P.: Compositional pre-processing for automated reasoning in dependent type theory. In: CPP. pp. 63\u201377. ACM (2023)","DOI":"10.1145\/3573105.3575676"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Cohen, C., Crance, E., Mahboubi, A.: Trocq: proof transfer for free, with or without univalence. In: Weirich, S. (ed.) Programming Languages and Systems. LNCS, vol. 14576, pp. xx\u2013yy. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57262-3_10","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Cohen, C., Crance, E., Mahboubi, A.: coq-community\/trocq: Trocq 0.1.5 (Jan 2024). https:\/\/doi.org\/10.5281\/zenodo.10563382","DOI":"10.5281\/zenodo.10563382"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: CPP. LNCS, vol.\u00a08307, pp. 147\u2013162. Springer (2013)","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in coq. In: ITP. LNCS, vol.\u00a07406, pp. 83\u201398. Springer (2012)","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$Prolog interpreter. In: LPAR. LNCS, vol.\u00a09450, pp. 460\u2013468. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"11_CR10","unstructured":"Fr\u00fchwirth, T., Raiser, F.: Constraint handling rules: Compilation, execution, and analysis (2011)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Krauss, A., Kuncar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: ITP. LNCS, vol.\u00a07998, pp. 100\u2013115. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kuncar, O.: Lifting and transfer: A modular design for quotients in Isabelle\/HOL. In: CPP. LNCS, vol.\u00a08307, pp. 131\u2013146. Springer (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"11_CR13","unstructured":"Krishnaswami, N.R., Dreyer, D.: Internalizing relational parametricity in the extensional calculus of constructions. In: CSL. LIPIcs, vol.\u00a023, pp. 432\u2013451. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Lammich, P.: Automatic data refinement. In: ITP. LNCS, vol.\u00a07998, pp. 84\u201399. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Lammich, P., Lochbihler, A.: Automatic refinement to efficient data structures: A comparison of two approaches. J. Autom. Reason. 63(1), 53\u201394 (2019)","DOI":"10.1007\/s10817-018-9461-9"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Magaud, N.: Changing data representation within the Coq System. In: TPHOLs. LNCS, vol.\u00a02758, pp. 87\u2013102. Springer (2003)","DOI":"10.1007\/10930755_6"},{"key":"11_CR17","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. J. Formaliz. Reason. 2(1), 41\u201362 (2009)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N., Winterhalter, T.: The metacoq project. J. Autom. Reason. 64(5), 947\u2013999 (2020)","DOI":"10.1007\/s10817-019-09540-0"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Tabareau, N., Tanter, \u00c9., Sozeau, M.: The marriage of univalence and parametricity. Journal of the ACM (JACM) 68(1), 1\u201344 (2021)","DOI":"10.1145\/3429979"},{"key":"11_CR20","unstructured":"Tassi, E.: Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi $$\\lambda $$prolog). In: CoqPL (January 2018), https:\/\/hal.inria.fr\/hal-01637063"},{"key":"11_CR21","unstructured":"Zimmermann, T., Herbelin, H.: Automatic and transparent transfer of theorems along isomorphisms in the coq proof assistant. In: CICM (Work in Progress). pp. 50\u201362 (2015)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57262-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:04:52Z","timestamp":1712214292000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57262-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572616","9783031572623"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57262-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/esop\/","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":"72","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":"25","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":"1","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":"35% - 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.2","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":"8","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":"The proceedings also contain 4 artifact report that have not been part of the original submission","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)"}}]}}