{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:41Z","timestamp":1780994801656,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":27,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["FMiTF-1918396"],"award-info":[{"award-number":["FMiTF-1918396"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-20-C-0107"],"award-info":[{"award-number":["HR0011-20-C-0107"]}],"id":[{"id":"10.13039\/100000185","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.3575670","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"303-319","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["P4Cub: A Little Language for Big Routers"],"prefix":"10.1145","author":[{"given":"Rudy","family":"Peterson","sequence":"first","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric Hayden","family":"Campbell","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Chen","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natalie","family":"Isak","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Calvin","family":"Shyu","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan","family":"Doenges","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Parisa","family":"Ataei","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544220"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3565475.3569081"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Andrew W Appel Lennart Beringer Qinxiang Cao and Josiah Dodds. 2016. Verifiable C. https:\/\/doi.org\/10.1007\/s10817-018-9457-5 10.1007\/s10817-018-9457-5","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338919"},{"key":"e_1_3_2_1_6_1","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21)","author":"Campbell Eric Hayden","year":"2021","unstructured":"Eric Hayden Campbell, William T Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soul\u00e9, and Nate Foster. 2021. Avenir: Managing data plane diversity with control plane synthesis. In 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI 21). 133\u2013153."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434322"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7495829"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523715"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Matthias Eichholz Eric Campbell Nate Foster Guido Salvaneschi and Mira Mezini. 2019. How to avoid making a billion-dollar mistake: Type-safe data plane programming with SafeP4. ECOOP https:\/\/doi.org\/10.48550\/ARXIV.1906.07223","DOI":"10.48550\/ARXIV.1906.07223"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498701"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360220"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Ali Kheradmand and Grigore Rosu. 2018. P4K: A formal semantics of P4 and applications. arXiv preprint arXiv:1804.01468 https:\/\/doi.org\/10.48550\/arXiv.1804.01468","DOI":"10.48550\/arXiv.1804.01468"},{"key":"e_1_3_2_1_17_1","volume-title":"The BSD conference. 5, 1\u201320","author":"Lattner Chris","year":"2008","unstructured":"Chris Lattner. 2008. LLVM and Clang: Next generation compiler technology. In The BSD conference. 5, 1\u201320."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2002.11054"},{"key":"e_1_3_2_1_20_1","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_22_1","unstructured":"P4 Language Consortium. 2022. P4 16 language specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v-1.2.3.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3554345"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472937"},{"key":"e_1_3_2_1_26_1","volume-title":"Appel","author":"Wang Qinshi","year":"2022","unstructured":"Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Rudy Peterson, Lennart Beringer, and Andrew W. Appel. 2022. Verifiable P4 : A Foundational Verifier for Stateful P4 Programs. Sept., Unpublished manuscript; submitted for publication."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103709"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Boston MA USA","acronym":"CPP '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"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.3575670","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575670","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575670","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:37Z","timestamp":1750178737000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575670"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":27,"alternative-id":["10.1145\/3573105.3575670","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575670","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"}}]}}