{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:47Z","timestamp":1750309187388,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Ministry of Science, Innovation and Universities, Spain","award":["RTC-2017-6740-7"],"award-info":[{"award-number":["RTC-2017-6740-7"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636958","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"2-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["UTC Time, Formally Verified"],"prefix":"10.1145","author":[{"given":"Ana","family":"de Almeida Borges","sequence":"first","affiliation":[{"name":"University of Barcelona, Barcelona, Spain \/ Formal Vindications S.L., Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mireia","family":"Gonza\u0301lez Bedmar","sequence":"additional","affiliation":[{"name":"University of Barcelona, Barcelona, Spain \/ Formal Vindications S.L., Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan","family":"Conejero Rodr\u00edguez","sequence":"additional","affiliation":[{"name":"University of Barcelona, Barcelona, Spain \/ Formal Vindications S.L., Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eduardo","family":"Hermo Reyes","sequence":"additional","affiliation":[{"name":"University of Barcelona, Barcelona, Spain \/ Formal Vindications S.L., Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joaquim","family":"Casals Bu\u00f1uel","sequence":"additional","affiliation":[{"name":"University of Barcelona, Barcelona, Spain \/ Formal Vindications S.L., Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost","family":"Joosten","sequence":"additional","affiliation":[{"name":"University of Barcelona, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022","author":"de Almeida Borges Ana","year":"2022","unstructured":"Ana de Almeida Borges. 2022. Towards a Coq formalization of a quantified modal logic. In Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022), Christoph Benzm\u00fcller and Jens Otten (Eds.). CEUR, Haifa, Israel, 13\u201327. https:\/\/ceur-ws.org\/Vol-3326\/ARQNL2022_paper1.pdf"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580430"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104636"},{"key":"e_1_3_2_1_4_1","unstructured":"Ana de Almeida Borges Guillaume Melquiond and Pierre Roux. 2021. Signed primitive integers. https:\/\/github.com\/coq\/coq\/pull\/13559"},{"key":"e_1_3_2_1_5_1","unstructured":"Android. 2022. Date Class. Android Reference Manual. https:\/\/developer.android.com\/reference\/java\/util\/Date"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503951"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90005-2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.9"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.060"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993526"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.34"},{"volume-title":"Resolutions of the General Conference on Weights and Measures (27th meeting). https:\/\/www.bipm.org\/documents\/20126\/77765681\/Resolutions-2022","author":"Comit\u00e9","key":"e_1_3_2_1_18_1","unstructured":"Comit\u00e9 international des poids et mesures. 2022. Resolutions of the General Conference on Weights and Measures (27th meeting). https:\/\/www.bipm.org\/documents\/20126\/77765681\/Resolutions-2022.pdf\/281f3160-fc56-3e63-dbf7-77b76500990f"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.006"},{"key":"e_1_3_2_1_20_1","unstructured":"Coq Development Team. 2023. Coq.ssr.ssreflect. Coq Standard Library Version 8.17.1. https:\/\/coq.inria.fr\/doc\/V8.17.1\/stdlib\/Coq.ssr.ssreflect.html"},{"key":"e_1_3_2_1_21_1","unstructured":"Coq Development Team. 2023. Programmable proof search. Coq Reference Manual Version 8.17.1. https:\/\/coq.github.io\/doc\/v8.17\/refman\/proofs\/automatic-tactics\/auto.html"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_11"},{"key":"e_1_3_2_1_23_1","unstructured":"cppreference.com Team. 2021. utc_clock. C++ Reference Manual. https:\/\/en.cppreference.com\/mwiki\/index.php?title=cpp\/chrono\/utc_clock&oldid=134878"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_3"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2677006"},{"key":"e_1_3_2_1_26_1","unstructured":"William DeMeo. 2022. The Agda Universal Algebra Library. http:\/\/ualib.org\/"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"e_1_3_2_1_28_1","volume-title":"COMMISSION IMPLEMENTING REGULATION (EU) 2016\/799 of","author":"European Parliament and Council of the European Union. 2016.","year":"2016","unstructured":"European Parliament and Council of the European Union. 2016. COMMISSION IMPLEMENTING REGULATION (EU) 2016\/799 of 18 March 2016 implementing Regulation (EU) No 165\/2014 of the European Parliament and of the Council laying down the requirements for the construction, testing, installation, operation and repair of tachographs and their components. Official Journal of the European Union. https:\/\/eur-lex.europa.eu\/legal-content\/EN\/TXT\/?uri=CELEX"},{"key":"e_1_3_2_1_29_1","unstructured":"Formal Vindications S.L. 2022. How-To: Use of the FV Time Manager on Windows Linux and other platforms through its command line interface. https:\/\/formalv.gitlab.io\/fv-docs\/fvtm-tech-spec.pdf"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294091"},{"key":"e_1_3_2_1_31_1","first-page":"1382","article-title":"Formal proof \u2013 the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier. 2008. Formal proof \u2013 the four-color theorem. Notices of the American Mathematical Society 55, 11 (2008), 1382\u20131393.","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_33_1","unstructured":"Mireia Gonz\u00e1lez Bedmar. 2022. A method for clean extraction: example. https:\/\/gitlab.com\/formalv\/extraction-model"},{"key":"e_1_3_2_1_34_1","unstructured":"Google. 2022. Unsmear. https:\/\/github.com\/google\/unsmear"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_9"},{"key":"e_1_3_2_1_39_1","unstructured":"Howard Hinnant. 2019. chrono-Compatible Low-Level Date Algorithms. https:\/\/howardhinnant.github.io\/date_algorithms.html"},{"key":"e_1_3_2_1_40_1","unstructured":"IEEE and The Open Group. 2018. The Open Group Base Specifications Issue 7. https:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/"},{"key":"e_1_3_2_1_41_1","unstructured":"IETF. 2016. Leap seconds list. https:\/\/www.ietf.org\/timezones\/data\/leap-seconds.list"},{"key":"e_1_3_2_1_42_1","volume-title":"Recommendation ITU-R TF.460-6: Standard-frequency and time-signal emissions","author":"Radiocommunication Assembly ITU","year":"2002","unstructured":"ITU Radiocommunication Assembly. 2002. Recommendation ITU-R TF.460-6: Standard-frequency and time-signal emissions. International Telecommunication Union (2002). https:\/\/www.itu.int\/dms_pubrec\/itu-r\/rec\/tf\/R-REC-TF.460-6-200202-I!!PDF-E.pdf"},{"key":"e_1_3_2_1_43_1","unstructured":"Daan Leijen. 2016. UTC time calculation. The Koka Programming Language Documentation. https:\/\/koka-lang.github.io\/koka\/doc\/std_time_utc.html"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_12"},{"key":"e_1_3_2_1_46_1","unstructured":"Pierre Letouzey. 2004. Programmation fonctionnelle certifi\u00e9e: l\u2019extraction de programmes dans l\u2019assistant Coq. Ph. D. Dissertation. Universit\u00e9 Paris Sud-Paris XI."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1088\/1681-7575\/ac9da5"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_1"},{"key":"e_1_3_2_1_50_1","unstructured":"Mathematical Components Team. 2007. The Mathematical Components library. https:\/\/math-comp.github.io\/"},{"key":"e_1_3_2_1_51_1","unstructured":"MathWorks. 2022. leapseconds. MATLAB Reference Manual. https:\/\/www.mathworks.com\/help\/matlab\/ref\/leapseconds.html"},{"key":"e_1_3_2_1_52_1","unstructured":"Guillaume Melquiond. 2023. Coq Interval. https:\/\/coqinterval.gitlabpages.inria.fr\/"},{"key":"e_1_3_2_1_53_1","unstructured":"Microsoft. 2022. DateTime.Ticks. Microsoft .NET 6 Documentation. https:\/\/docs.microsoft.com\/en-us\/dotnet\/api\/system.datetime.ticks?view=net-6.0"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_8"},{"key":"e_1_3_2_1_55_1","unstructured":"Kazuhiko Sakaguchi. 2021. Mczify. https:\/\/github.com\/math-comp\/mczify"},{"key":"e_1_3_2_1_56_1","volume-title":"Nicolas Tabareau, and Th\u00e9o Winterhalter.","author":"Sozeau Matthieu","year":"2023","unstructured":"Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Th\u00e9o Winterhalter. 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. (2023). https:\/\/inria.hal.science\/hal-04077552 hal-04077552."}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"London UK","acronym":"CPP '24"},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636958","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636958","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636958"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":56,"alternative-id":["10.1145\/3636501.3636958","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636958","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}