{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T01:42:48Z","timestamp":1787017368886,"version":"build-2736575974"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing \u03a04, a dependently-typed version of P4 based on decidable refinements. We motivate the design of \u03a04, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.<\/jats:p>","DOI":"10.1145\/3498701","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Dependently-typed data plane programming"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6112-9305","authenticated-orcid":false,"given":"Matthias","family":"Eichholz","sequence":"first","affiliation":[{"name":"TU Darmstadt, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5954-2136","authenticated-orcid":false,"given":"Eric Hayden","family":"Campbell","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2508-1428","authenticated-orcid":false,"given":"Matthias","family":"Krebs","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6563-7537","authenticated-orcid":false,"given":"Mira","family":"Mezini","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ANCS.2019.8901893"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3422604.3425930"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/182409.182431"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486011"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535840"},{"key":"e_1_2_2_8_1","unstructured":"Cisco. 2018. Cisco Nexus 3000 Series Switches. https:\/\/www.cisco.com\/c\/en\/us\/products\/switches\/nexus-3000-series-switches\/index.html  Cisco. 2018. Cisco Nexus 3000 Series Switches. https:\/\/www.cisco.com\/c\/en\/us\/products\/switches\/nexus-3000-series-switches\/index.html"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_35"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434322"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405888"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.12"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_15"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065046"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405879"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_8"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281443"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/767193.767195"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3289602.3293924"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706347"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132764"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_2_2_26_1","unstructured":"Conor McBride. 2001. The derivative of a regular type is its type of one-hole contexts. Extended abstract available at http:\/\/strictlypositive.org\/diff.pdf  Conor McBride. 2001. The derivative of a regular type is its type of one-hole contexts. Extended abstract available at http:\/\/strictlypositive.org\/diff.pdf"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/347059.347563"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868447.1868456"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_32_1","volume-title":"EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In USENIX Security Symposium (USENIX Security). 1465\u20131482","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro , Antoine Delignat-Lavaud , Cedric Fournet , Nikhil Swamy , Tej Chajed , Nadim Kobeissi , and Jonathan Protzenko . 2019 . EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In USENIX Security Symposium (USENIX Security). 1465\u20131482 . isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud Tahina Ramananandro, Antoine Delignat-Lavaud, Cedric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In USENIX Security Symposium (USENIX Security). 1465\u20131482. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405872"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276502"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3050220.3050234"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855785"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507657"},{"key":"e_1_2_2_43_1","volume-title":"Dependent Types in Practical Programming. In Symposium on Principles of Programming Languages (POPL). 214\u2013227","author":"Xi Hongwei","year":"1999","unstructured":"Hongwei Xi and Frank Pfenning . 1999 . Dependent Types in Practical Programming. In Symposium on Principles of Programming Languages (POPL). 214\u2013227 . isbn:1581130953 Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In Symposium on Principles of Programming Languages (POPL). 214\u2013227. isbn:1581130953"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498701","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498701","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:28Z","timestamp":1750174228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498701"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498701"],"URL":"https:\/\/doi.org\/10.1145\/3498701","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}