{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:05Z","timestamp":1750219805986,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":10,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["J 4386"],"award-info":[{"award-number":["J 4386"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575686","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"135-147","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Terms for Efficient Proof Checking and Parsing"],"prefix":"10.1145","author":[{"given":"Michael","family":"F\u00e4rber","sequence":"first","affiliation":[{"name":"University of Innsbruck, Austria"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"volume-title":"A framework for defining computational higher-order logics. (Un cadre de d\u00e9finition de logiques calculatoires d\u2019ordre sup\u00e9rieur). Ph. D. Dissertation. \u00c9cole Polytechnique","author":"Assaf Ali","key":"e_1_3_2_1_1_1","unstructured":"Ali Assaf. 2015. A framework for defining computational higher-order logics. (Un cadre de d\u00e9finition de logiques calculatoires d\u2019ordre sup\u00e9rieur). Ph. D. Dissertation. \u00c9cole Polytechnique, Palaiseau, France. https:\/\/tel.archives-ouvertes.fr\/tel-01235303"},{"key":"e_1_3_2_1_2_1","unstructured":"Ali Assaf Guillaume Burel Rapha\u00ebl Cauderlier David Delahaye Gilles Dowek Catherine Dubois Fr\u00e9d\u00e9ric Gilbert Pierre Halmagrand Olivier Hermant and Ronan Saillard. [n. d.]. Dedukti: a Logical Framework based on the \u03bb \u03a0 -Calculus Modulo Theory. http:\/\/www.lsv.ens-cachan.fr\/~dowek\/Publi\/expressing.pdf"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503683"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Michael F\u00e4rber. 2021. Proofs from interactive and automated theorem provers to evaluate Kontroli & Dedukti. https:\/\/doi.org\/10.5281\/zenodo.5729640 10.5281\/zenodo.5729640","DOI":"10.5281\/zenodo.5729640"},{"volume-title":"Extending higher-order logic with predicate subtyping: Application to PVS. (Extension de la logique d\u2019ordre sup\u00e9rieur avec le sous-typage par pr\u00e9dicats). Ph. D. Dissertation","author":"Gilbert Fr\u00e9d\u00e9ric","key":"e_1_3_2_1_6_1","unstructured":"Fr\u00e9d\u00e9ric Gilbert. 2018. Extending higher-order logic with predicate subtyping: Application to PVS. (Extension de la logique d\u2019ordre sup\u00e9rieur avec le sous-typage par pr\u00e9dicats). Ph. D. Dissertation. Sorbonne Paris Cit\u00e9, France. https:\/\/tel.archives-ouvertes.fr\/hal-01673518"},{"key":"e_1_3_2_1_7_1","volume-title":"Automated Deduction and Proof Certification for the B Method. (D\u00e9duction Automatique et Certification de Preuve pour la M\u00e9thode B). Ph. D. Dissertation. Conservatoire national des arts et m\u00e9tiers","author":"Halmagrand Pierre","year":"2046","unstructured":"Pierre Halmagrand. 2016. Automated Deduction and Proof Certification for the B Method. (D\u00e9duction Automatique et Certification de Preuve pour la M\u00e9thode B). Ph. D. Dissertation. Conservatoire national des arts et m\u00e9tiers, Paris, France. https:\/\/tel.archives-ouvertes.fr\/tel-01420460"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_13"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165195"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.5"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575686","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575686","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575686"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":10,"alternative-id":["10.1145\/3573105.3575686","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575686","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}