Pith. sign in

REVIEW 4 major objections 5 minor 47 references

P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification

T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read P4-SpecTec makes P4's specification a single executable source of truth that generates a type checker, interpreter, and prose document.

desk verdict A credible, well-documented mechanization of P4 v1.2.5 that deserves serious refereeing, but the 100% pass rate is more scoped than the text sometimes lets on. read the letter →

arxiv 2608.00639 v1 pith:BPBFNQI4 submitted 2026-08-01 cs.PL

Jaehyun Lee , Seokhun Jeong , Sehyuk Ahn , Haechan Kwon , Sukyoung Ryu This is my paper
classification cs.PL
keywords P4languagemechanizationexecutablespecificationalgorithmicinferencerulestypesystemsoperationalsemanticstoolingprogramminglanguages
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to show that a real-world programming language can be maintained from a single mechanized specification even when no normative specification exists, using P4 as the test case. It introduces algorithmic inference rules — inference rules whose inputs, outputs, and order are made explicit — so that one mechanized definition can be executed as a P4 type checker and interpreter and also rendered as a readable prose specification. The claim is that this works at full P4 v1.2.5 scale: after excluding tests tied to unimplemented features or known external issues, the generated tools pass the reference compiler's entire test suite. The paper also reports 24 bugs found in the official P4 specification and reference compiler, and states the P4 working group has conditionally adopted the framework as the official authoring toolchain. If correct, it establishes a template for moving languages without normative specs onto a mechanized, executable, community-owned specification.

What carries the argument

The load-bearing instrument is algorithmic inference rules, a computational subset of ordinary inference rules. Each rule must satisfy explicit dataflow constraints — inputs are declared by a hint, premises are ordered, existential witnesses are disallowed, and bindings are required to be invertible — so that proof search becomes a deterministic backtracking procedure. The same rules are then structured into a control-flow form, which removes redundant evaluation and becomes the basis for both the executable backends and the generated prose algorithms; external, target-specific behavior is handled by an opaque state mechanism that lets the mechanized semantics interact with outside implement

What would settle it

Run the generated type checker on every P4 v1.2.5 program in the reference compiler's test suite without exclusions; any non-excluded program that the checker rejects while the compiler accepts, or any executed program that emits a different packet than the simulator predicts, would falsify the coverage claim.

Watch

Extended reading notes

Core claim

The paper's central claim is that P4 — a language evolving without a normative specification — can be captured in one mechanized source that is simultaneously executable and readable. The key move is to define the semantics as algorithmic inference rules: rules that are deterministic and have explicit dataflow, so they can be directly run by a backtracking meta-interpreter without a separate translation step. Running those rules yields an executable P4 type checker, instantiation engine, and interpreter; compiling the same rules yields the prose algorithms for the official specification document. The paper reports that, after excluding tests tied to features not yet standardized or to known

Load-bearing premise

The load-bearing premise is that the reference compiler's test suite, after the study's exclusions, is a faithful proxy for P4 v1.2.5 semantics; if the omitted tests hide real semantic gaps, the completeness claims, the bug count, and the adoption argument all weaken.

Editorial extensions

If this is right

  • Future P4 releases can be specified by editing one mechanized source; type checker, interpreter, and prose document are regenerated from it.
  • A mechanized spec with an executable type system can serve as a test oracle, as demonstrated by the 24 specification/compiler inconsistencies it surfaced.
  • The generated prose specification can coexist with the existing informal document via splice anchors, letting a community transition incrementally.
  • Because the type system is executable, static and dynamic semantics can be validated on the same corpus, which earlier formalizations could not do.
  • P4-SpecTec's conditional adoption means the P4 standardization process moves to a test-validated, tool-generated specification workflow.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same pattern should transfer to other domain-specific languages that lack normative specs, provided their semantics can be expressed with deterministic, dataflow-explicit rules; the open-world extern mechanism already handles languages with target-defined runtime behavior.
  • The p4c test suite's exclusions suggest that the claimed completeness is bounded by test coverage; a natural next step is to generate semantic-coverage measures or fuzz P4 programs to seek non-excluded divergences.
  • If adopted long-term, the mechanized spec could become a shared artifact for compiler implementers and hardware vendors, reducing the silent divergence that currently accumulates.
  • The prose-hint and rule-group mechanism points toward a workflow where formal rules and natural-language intuition coexist, which may ease adoption in communities without a formal-methods background.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper presents P4-SpecTec, a language-mechanization framework for P4 built on the SpecTec meta-language. The authors introduce algorithmic inference rules as an executable and documentable specification medium, and use them to mechanize the syntax, type system, static instantiation phase, and big-step dynamic semantics of P4 v1.2.5. From this single mechanized source they derive a P4 type checker, an instantiation engine, an interpreter, and a prose specification document. The framework is evaluated against the p4c test suite: after excluding tests classified as Future, P4Spec, P4C, or Specific, and after patching two STF files, the generated backends pass all remaining positive and negative static tests and all dynamic tests. The paper reports 24 specification/compiler bugs found during the process, compares coverage with Petr4 and HOL4P4, and reports that the P4 LDWG has conditionally adopted P4-SpecTec as the official specification authoring toolchain.

Significance. If the central claims hold, this is a substantial contribution to language mechanization: it is the first end-to-end case of integrating a mechanized executable specification into a real-world language that lacks a normative specification, and it demonstrates that an executable type system can be included in such a framework, which neither ESMeta nor Wasm-SpecTec supports. The engineering artifact is large and concrete (28,862 lines, 1,090 rules, 561 definitions), and the paper makes machine-checked execution, reproducible test results, and specific bug reports central to its argument. The socio-technical integration story is also valuable. However, the completeness claim is weakened by the evaluation design: the specification and the test oracle co-evolve (through SP1–SP9 amendments and test exclusions), and negative tests are not checked for the reason of rejection. These issues do not invalidate the framework's utility, but they do affect the strength of the paper's headline claims.

major comments (4)
  1. [§8.2, Tables 2–4; §8.5 (SP7, SP8)] The claim that the mechanization captures P4 v1.2.5 semantics is not independently established by the reported 100% pass rate. The pass rates are computed after excluding 134 static and 56 dynamic tests, and the excluded categories are not all out-of-scope: P4Spec tests are described as cases where the specification is under-specified or inconsistent with practice, and P4C tests are cases of suspected p4c non-conformance. At the same time, the paper amends the specification to match p4c practice (notably SP7, which alone affects 98 Pos tests). The validation target and validation data therefore co-evolve. The paper should report the results with and without the P4Spec/P4C exclusions, justify each such exclusion individually, and use an independently authored or held-out test set to support the completeness claim. As written, the 100% pass rate is a scoped consistency result, not a comple
  2. [§8.2, paragraph on negative tests] Negative tests are considered passing whenever the type checker rejects the program, regardless of the reason for rejection. A program may be rejected for a spurious reason (e.g., a parser limitation, an unrelated type error, or an overly conservative rule) even when the intended semantic error is not detected. Since the paper uses 521/521 Neg as evidence for the adequacy of the algorithmic type system, the evaluation should at least sample negative tests and verify that rejection occurs for the intended reason, for instance by checking p4c's expected diagnostics or by differential comparison with p4c on a held-out set. Without this, the negative-test result is substantially weaker than presented.
  3. [§8.1, parser adaptation] The paper claims the mechanization covers the concrete syntax of P4, but the evaluation uses an adapted Petr4 parser to parse P4 programs into meta-values rather than a parser generated from the mechanized grammar. This means the syntax portion of the mechanization is not exercised end-to-end, and syntax-related bugs in the mechanized grammar could be masked by the external parser. The authors should either generate the parser from the mechanized concrete syntax, or explicitly scope the syntax claim to the grammar definition and not to parsing validation.
  4. [§4.1 and §8.2, determinism validation] Algorithmic inference rules are defined as requiring determinism, but determinism is only checked dynamically when the -det flag is used during execution, not by the static validation described in §4.1. The paper acknowledges this is hard to check statically, yet the executable backends' default mode applies the first applicable rule without reporting ambiguity. This is a real limitation for a normative specification: a non-deterministic rule that is never triggered by the test suite will silently implement an arbitrary choice. The paper should state this limitation more prominently and, ideally, provide an estimate of how many rules were actually covered by -det execution during validation.
minor comments (5)
  1. [Table 7] The columns for SP entries show section numbers such as 'SP11294 7.2.8' but the PR/Issue links are not clearly separated; this makes the table hard to parse. Consider restructuring with explicit columns for PR number, spec section, and description.
  2. [§1.3 and throughout] The claims 'first end-to-end case study' and 'first executable mechanization' are strong. They should be accompanied by a precise definition of what 'end-to-end' and 'executable' include, so that the comparison with earlier work (Petr4, HOL4P4, Centaur) is not debatable on terminology.
  3. [§8.4 and Table 6] The comparison with Petr4 and HOL4P4 uses the same excluded-test set that was tuned for P4-SpecTec. The exclusions and STF patches should be applied uniformly to all tools, and the paper should state whether the excluded tests are also excluded for Petr4 and HOL4P4; otherwise Table 6 may overstate the coverage gap.
  4. [§8.3, Fig. 16] Execution times are reported from a single run. For a performance claim about IL vs. SL structuring, median or multiple-run statistics would be more robust.
  5. [Throughout] There are several self-referential or pipeline-related artifacts in the text, such as 'SP7128 7.2.8' and 'Footnote 2' placement. Please proofread the final version carefully.

Circularity Check

2 steps flagged · score 4.0 of 10

Validation is partly circular: SP7/SP8 amend the spec to match p4c tests, and P4Spec/P4C exclusions remove contested semantics before the 100% pass rate is reported; central mechanization still has independent content.

  1. fitted input called prediction [§7 (Integration) and §8.5 (RQ4, Table 7, SP7)]
    "In some cases, we amended the official specification to better reflect real-world practice through LDWG discussions. ... SP7 in particular was significant, as 98 tests from Pos rely on implicit casting of call arguments."

    The specification that P4-SpecTec mechanizes is partly fitted to the p4c test suite: SP7 changes the P4 spec to allow implicit casts because 98 positive tests require it. The same suite is then used in §8.2 as the independent arbiter validating the mechanization, and the 98 tests count toward the reported 100% pass rate. Thus the validation result is partly an artifact of adjusting the spec to the benchmark: the data used to define the semantics is the same data used to confirm it. This is not total circularity (the bulk of the 28,862-line mechanization comes from the spec and LDWG discussions), but the specific claim that the p4c suite independently validates completeness is weakened.

  2. other [§8.2, Table 2]
    "P4Spec: Under discussion with the LDWG; semantics is under-specified or inconsistent with practice. P4C: Under discussion with p4c developers regarding non-conformance to the P4 specification."

    The evaluation excludes the very categories in which the mechanization's semantic choices are contested: under-specified spec areas and p4c non-conformances. After removing these, the reported 100% pass rate is a statement only about the uncontested remainder; it cannot validate the mechanization's resolution of the disputed cases. The disputed cases later appear as the paper's 'bugs found' (SP/CB), so the pass rate and bug count jointly define the semantics rather than independently confirming it. The paper discloses the exclusions and discusses their subjectivity in §8.6, so this is partial circularity in the validation argument rather than a hidden derivation loop.

full rationale

The central technical claims—algorithmic inference rules, executability of the P4 type system, generation of a prose spec, and comparison against Petr4/HOL4P4—do not reduce to the evaluation data. The mechanization was built from the informal P4 spec and LDWG engagement, and the p4c suite is an external artifact; prior formalizations also fail many of the same tests, so P4-SpecTec's better coverage is genuine. However, the completeness/correctness validation is partly circular: the spec was amended (SP7, SP8) to match p4c practice, and tests revealing under-specification or p4c non-conformance are excluded before reporting 100% pass. The negative-test criterion (rejection without checking the reason) further weakens semantic validation but is a correctness threat, not circularity. The paper's own §8.6 admits the p4c suite 'is not a guarantee of its correctness.' No load-bearing self-citation or imported uniqueness theorem appears: Wasm-SpecTec is reused as infrastructure, not as the justification for P4 semantics. Overall score 4: partial circularity in the validation loop, with substantial independent content in the framework and bug reports.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

No numeric constants are fitted to data; the P4Testgen cap of 10 is the only hand-chosen number that directly affects coverage. The load-bearing assumptions are all methodological or scoping choices: the p4c suite as oracle, dynamic determinism checking, no concurrency, simulator fidelity, and test-based semantics preservation. No new physical or formal entities are postulated.

free parameters (1)
  • P4Testgen per-program test cap = 10
    Section 8.1 says up to 10 STF tests per P4 program are generated; this hand-chosen cap bounds the dynamic-semantics coverage and is not derived from any coverage criterion.
assumptions (5)
  • domain assumption The p4c test suite, after exclusions and patches, is a valid proxy for P4 v1.2.5 semantics.
    Invoked in §8.1–8.2 and defended only loosely in §8.6; if false, the completeness and correctness claims do not follow.
  • ad hoc to paper Dynamic -det validation is sufficient to justify the determinism of algorithmic inference rules.
    §4.1 paragraph 5 concedes static mutual-exclusion checks are non-trivial; only exercised programs are checked, so unexercised non-determinism may remain.
  • domain assumption Big-step semantics without concurrency captures the intended P4 semantics for the supported scope.
    §2.2/Table 1: concurrency is excluded because LDWG discussions are at an early stage; this is a scope choice rather than a proven equivalence.
  • domain assumption Architecture simulators for V1Model, eBPF, and PSA faithfully model target extern behavior.
    §8.1: simulators are plugged in via ext relations; interpreter-backend results depend on their fidelity.
  • ad hoc to paper The EL-to-IL elaboration and anti-unification-based structuring preserve the intended semantics.
    §5 and §8.3: semantics preservation is validated by test results on the chosen suite, not by a formal proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification." pith.science (2026). https://pith.science/paper/BPBFNQI4

@misc{pith2026260800639,
  author       = {Pith},
  title        = {Pith review of: P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/BPBFNQI4}},
  note         = {Machine review of arXiv:2608.00639}
}
read the original abstract

Programming languages evolve, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and WebAssembly (Wasm) specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain.

Figures

Figures reproduced from arXiv: 2608.00639 by the authors.

Figure 1
Figure 1. (Left) ESMeta operating downstream of the ECMAScript specification, parsing and reconstructing it. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. (Top) Mechanization of the P4 if statement. (Bottom) P4-SpecTec backends. redesigning the backends to accommodate P4’s distinct features. As shown in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. VSS architecture diagram. 1 extern packet_in { 2 void extract<T>(out T hdr); 3 } 4 extern packet_out { 5 void emit<T>(in T hdr); 6 } 7 struct Meta { 8 bit<8> inport; bit<8> outport; bool drop; 9 } 10 parser Parse<H>(packet_in p, out H hdr, 11 inout Meta meta); 12 control Control<H>(inout H hdr, 13 inout Meta meta); 14 control Deparse<H>(packet_out p, in H hdr); 15 package VSS<H>(Parse<H> parse, 16 Control<H> ctrl, 1… view at source ↗
Figures from the paper (10 more)
Figure 5
Figure 5. Figure 5: A program for VSS architecture (switch.p4). deparser. Packets enter the pipeline, where they are either emitted after deparsing or dropped during match-action. The three stages are programmable via P4. Besides the programmable components, each target also has its speci…
Figure 6
Figure 6. Figure 6: P4 abstract syntax in P4-SpecTec (simplified). [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 8
Figure 8. Figure 8: P4 typing and instantiation (simplified). [PITH_FULL_IMAGE:figures/full_fig_p008_8.png]
Figure 10
Figure 10. Figure 10: Overview of the P4-SpecTec architecture. [PITH_FULL_IMAGE:figures/full_fig_p010_10.png]
Figure 11
Figure 11. Figure 11: P4 if statement evaluation rules. condition is a list of exprs. Typing those is a premise (Expr_ok: TC |- expr : exprIR)*, meaning that for each expr in expr*, Expr_ok is applied to derive exprIR. exprIR are then collected into a list, exprIR*. Similarly, $typeof(expr…
Figure 12
Figure 12. Figure 12: Abstract syntax of IL 4. Precluding existentials. Existential meta-variables may appear in three ways in inference rules, and all of them are disallowed and checked for in the validation algorithm. Consider the following variants of let typeIR = $typeof(exprIR), bindi…
Figure 13
Figure 13. Figure 13: Evaluation rules for P4 statements. 4.2 Executing Algorithmic Inference Rules Having validated that the inference rules are algorithmic, implementing a meta-interpreter for them is relatively straightforward. Algorithms for evaluating relations and premises are availa…
Figure 14
Figure 14. Figure 14: Abstract syntax of SL Architectures differ in their pipeline stages and the set of supported externs. Therefore, archi￾tecture implementations are plugged in to P4-SpecTec, allowing to execute packet processing for different architectures while evaluating programmable…
Figure 15
Figure 15. Figure 15: An example STF file [PITH_FULL_IMAGE:figures/full_fig_p022_15.png]
Figure 16
Figure 16. Figure 16: Performance comparison of IL and SL interpreters on Pos for the P4 type checker and V1Model+ for the P4 interpreter. (Future) Features not yet standardized in P4 v1.2.5, e.g., compound assignments such as +=. (P4Spec) Under discussion with the LDWG; semantics is under…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

47 extracted references · 4 canonical work pages

  1. [1]

    https://github.com/es-meta/esmeta

    2022.ESMeta: An ECMAScript specification metalanguage used for automatically generating language-based tools. https://github.com/es-meta/esmeta

    2022

  2. [2]

    Kinan Dak Albab, Jonathan DiLorenzo, Stefan Heule, Ali Kheradmand, Steffen Smolka, Konstantin Weitz, Muhammad Timarzi, Jiaqi Gao, and Minlan Yu. 2022. SwitchV: automated SDN switch validation with P4 models. InProceedings of the ACM SIGCOMM 2022 Conference(Amsterdam, Netherlands)(SIGCOMM ’22). Association for Computing Machinery, New York, NY, USA, 365–37...

    arXiv 2022

  3. [3]

    Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, and Mads Dam. 2024. HOL4P4: Mechanized Small-Step Semantics for P4.Proc. ACM Program. Lang.8, OOPSLA1, Article 102 (April 2024), 27 pages. doi:10.1145/3649819

    work page doi:10.1145/3649819 2024

  4. [4]

    2024.P4-SpecTec – Mechanized Language Definition for P4

    Anonymous Author(s). 2024.P4-SpecTec – Mechanized Language Definition for P4

    2024

  5. [5]

    Gray, Robert M

    Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell

  6. [6]

    Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. 2019. Skeletal semantics and their interpretations. Proc. ACM Program. Lang.3, POPL, Article 44 (Jan. 2019), 31 pages. doi:10.1145/3290357

    doi:10.1145/3290357 2019

  7. [7]

    Denis Bogdanas and Grigore Roşu. 2015. K-Java: A Complete Semantics of Java. InProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). Association for Computing Machinery, New York, NY, USA, 445–456. doi:10.1145/2676726.2676982

    arXiv 2015

  8. [8]

    Borras, D

    P. Borras, D. Clement, Th. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. 1988. Centaur: the system. In Proceedings of the Third ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments(Boston, Massachusetts, USA)(SDE 3). Association for Computing Machinery, New York, NY, USA, 14–24. doi:10.1145/64135.65005

    arXiv 1988

Show all 47 references
  1. [9]

    Mihai Budiu and Chris Dodd. 2017. The P4 16 Programming Language.SIGOPS Oper. Syst. Rev.51, 1 (Sept. 2017), 5–14. doi:10.1145/3139645.3139648

    2017

  2. [10]

    Cerna and Temur Kutsia

    David M. Cerna and Temur Kutsia. 2023. Anti-unification and Generalization: A Survey. InProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, Edith Elkind (Ed.). International Joint Conferences on Artificial Intelligence Organiza...

    2023 doi

  3. [11]

    Thierry Despeyroux. 1984. Executable specification of static semantics. InSemantics of Data Types, Gilles Kahn, David B. MacQueen, and Gordon Plotkin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 215–233

    1984

  4. [12]

    Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. 2021. Petr4: formal foundations for p4 data planes.Proc. ACM Program. Lang.5, POPL, Article 41 (Jan. 2021), 3...

    2021 doi

  5. [13]

    Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing.ACM Comput. Surv.54, 5, Article 98 (May 2021), 38 pages. doi:10.1145/3450952

    2021 doi

  6. [14]

    2025.ECMA-262, 16th edition, ECMAScript®2025 Language Specification

    ECMA International. 2025.ECMA-262, 16th edition, ECMAScript®2025 Language Specification. https://262.ecma- international.org

    2025

  7. [15]

    2026.WebAssembly Specification (Release 3.0)

    Andreas Rossberg (editor). 2026.WebAssembly Specification (Release 3.0). https://webassembly.github.io/spec/core/

    2026

  8. [16]

    2009.Semantics Engineering with PLT Redex(1st ed.)

    Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009.Semantics Engineering with PLT Redex(1st ed.). The MIT Press

    2009

  9. [17]

    RISC-V Foundation. 2019. ISA Formal Spec Public Review. https://github.com/riscvarchive/ISA_Formal_Spec_Public_ Review

    2019

  10. [19]

    Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. arXiv:1804.01468 [cs.NI] https://arxiv.org/abs/1804.01468

    2018 arXiv

  11. [20]

    2026.P4 formalization using Ott and HOL4

    KTH STEP group. 2026.P4 formalization using Ott and HOL4. https://github.com/kth-step/HOL4P4

    2026

  12. [21]

    1997.The Definition of Standard ML (Revised)

    Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997.The Definition of Standard ML (Revised). 26

    1997

  13. [22]

    Louis Noizet and Alan Schmitt. 2022. Semantics in Skel and Necro. InProceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022 (CEUR Workshop Proceedings, Vol. 3284), Ugo Dal Lago and Daniele Gorla (Eds.). CEUR-WS.o...

    2022

  14. [23]

    2026.DOCA Documentation v2.10.0

    NVIDIA. 2026.DOCA Documentation v2.10.0. https://docs.nvidia.com/doca/archive/2-10-0/P4-Language-Support-in- DPL/index.html

    2026

  15. [24]

    2024.P4 Language Specification, Version 1.2.5

    P4 Language Consortium. 2024.P4 Language Specification, Version 1.2.5. https://p4.org/specs/

    2024

  16. [25]

    2026.P4 Governance

    P4 Language Consortium. 2026.P4 Governance. https://github.com/p4lang/p4c

    2026

  17. [26]

    2026.P4 Working Groups

    P4 Language Consortium. 2026.P4 Working Groups. https://p4.org/working-groups/

    2026

  18. [27]

    2026.P4_16 reference compiler

    P4 Language Consortium. 2026.P4_16 reference compiler. https://github.com/p4lang/p4c

    2026

  19. [28]

    2026.P4 Language Design Working Group Notes

    P4 Language Design Working Group. 2026.P4 Language Design Working Group Notes

    2026

  20. [29]

    Daejun Park, Andrei Stefănescu, and Grigore Roşu. 2015. KJS: a complete formal semantics of JavaScript. InProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation(Portland, OR, USA)(PLDI ’15). Association for Computing Machinery, New Yor...

    2015

  21. [30]

    Jihyeok Park, Seungmin An, and Sukyoung Ryu. 2022. Automatically deriving JavaScript static analyzers from specifi- cations using Meta-level static analysis. InProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Softwa...

    2022

  22. [31]

    Jihyeok Park, Seungmin An, Wonho Shin, Yusung Sim, and Sukyoung Ryu. 2022. JSTAR: JavaScript specification type analyzer using refinement. InProceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering(Melbourne, Australia)(ASE ’21). IEEE Press, ...

    2022

  23. [32]

    Jihyeok Park, Seungmin An, Dongjun Youn, Gyeongwon Kim, and Sukyoung Ryu. 2021. JEST: N+1-version Differential Testing of Both JavaScript Engines and Specification. InProceedings of the 43rd International Conference on Software Engineering(Madrid, Spain)(ICSE ’21). IEEE Press,...

    2021

  24. [33]

    Jihyeok Park, Jihee Park, Seungmin An, and Sukyoung Ryu. 2021. JISET: JavaScript IR-based semantics extraction toolchain. InProceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering(Virtual Event, Australia)(ASE ’20). Association for Computing...

    2021 doi

  25. [34]

    Alastair Reid. 2016. Trustworthy Specifications of ARM®V8-A and v8-M System Level Architecture. InProceedings of the 16th Conference on Formal Methods in Computer-Aided Design(Mountain View, California)(FMCAD ’16). FMCAD Inc, Austin, Texas, 161–168

    2016

  26. [35]

    Ekkehard Rohwedder and Frank Pfenning. 1996. Mode and termination checking for higher-order logic programs. InProgramming Languages and Systems — ESOP ’96, Hanne Riis Nielson (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 296–310

    1996

  27. [36]

    Andreas Rossberg. 2025. SpecTec has been adopted. https://webassembly.org/news/2025-03-27-spectec/

    2025

  28. [37]

    Grigore Ros,u and Traian Florin S, erbănută. 2010. An overview of the K semantic framework.The Journal of Logic and Algebraic Programming79, 6 (2010), 397–434. doi:10.1016/j.jlap.2010.03.012 Membrane computing and programming

    2010 doi

  29. [38]

    Fabian Ruffy, Jed Liu, Prathima Kotikalapudi, Vojtech Havel, Hanneli Tavante, Rob Sherwood, Vladyslav Dubina, Volodymyr Peschanenko, Anirudh Sivaraman, and Nate Foster. 2023. P4Testgen: An Extensible Test Oracle For P4. InProceedings of the ACM SIGCOMM 2023 Conference(New York...

    2023

  30. [39]

    Sukyoung Ryu and Jihyeok Park. 2024. JavaScript Language Design and Implementation in Tandem.Commun. ACM 67, 5 (May 2024), 86–95. doi:10.1145/3624723

    2024 doi

  31. [40]

    Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša

  32. [41]

    William Tu, Fabian Ruffy, and Mihai Budiu. 2018. P4C-XDP: Programming the linux kernel forwarding plane using P4. InLinux Plumbers Conference

    2018

  33. [42]

    2026.Petr4: Formal Semantics for P4

    Verified Network Toolchain. 2026.Petr4: Formal Semantics for P4. https://github.com/verified-network-toolchain/petr4

    2026

  34. [43]

    2025.frontend: Fix SpecializeGenericTypes

    Vladimír Štill. 2025.frontend: Fix SpecializeGenericTypes. https://github.com/p4lang/p4c/pull/5133

    2025

  35. [44]

    Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. 2023. Founda- tional Verification of Stateful P4 Packet Processing. In14th International Conference on Interactive Theorem Proving (ITP 2023)

    2023

  36. [45]

    Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, and Andreas Rossberg. 2024. Bringing the WebAssembly Standard up to Speed with SpecTec. PLDI (2024). 27

    2024

  37. [46]

    Dongjun Youn, Wonho Shin, and Sukyoung Ryu. 2025. WEST: Specification-Based Test Generation for WebAssembly. In2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE). 1403–1414. doi:10.1109/ ASE63991.2025.00119 28 Algorithm 5Relation evaluation 1:F...

    2025

  38. [2007]

    InProceedings of the 12th ACM SIGPLAN International Conference on Functional Programming(Freiburg, Germany)(ICFP ’07)

    Ott: effective tool support for the working semanticist. InProceedings of the 12th ACM SIGPLAN International Conference on Functional Programming(Freiburg, Germany)(ICFP ’07). Association for Computing Machinery, New York, NY, USA, 1–12. doi:10.1145/1291151.1291155

  39. [2019]

    ACM Program

    ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.Proc. ACM Program. Lang.3, POPL, Article 71 (Jan. 2019), 31 pages. doi:10.1145/3290384

    2019 doi

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.