RPLS 2025
who it's for
programming language researchers, specification engineers, verification engineers, compiler developers, JavaScript engine engineers, system software engineers, network dataplane engineers
topics
executable semantics generation; mechanized ECMAScript specification; WebAssembly mechanization in Isabelle; P4 symbolic execution testing; MiniRust operational semantics; lightweight hypervisor verification; Redex semantics engineering; SpecTec single source semantics; K framework executable semantics; production parser generation; automated dataplane test generation; provenance-annotated memory model
| title | author | length |
|---|---|---|
| Panel: Mechanized Specifications for Real-World Programming Languages | Sukyoung Ryu, Xiaohong Chen, Jonathan DiLorenzo, Michael Ficarra, Ralf Jung | 54m |
Panelists contrast concrete outcomes: an K framework built for engineering-first, executable semantics; a call for a usable symbolic executor for P4 that can… | ||
| Production Language Specification - Requirements for Multiple Usages | Peter Sewell | 27m |
Argues that one meta-language cannot serve all needs and surveys concrete tooling: LATeX/OCaml/Isabelle/HOL backends from LEM, a domain‑specific Sale front end… | ||
| MiniRust: A Core Language for Specifying Rust | Ralf Jung | 27m |
Two demos show concrete, reproducible failures: reading an uninitialized i8 decodes to an error and the interpreter flags undefined behavior at decode time… | ||
| Verification of WebAssembly Features | Philippa Gardner, Conrad Watt | 29m |
A mechanized WebAssembly semantics exists in Isabelle mechanization and parallel mechanizations target Rock/MetaRoc, with proven preservation and progress for… | ||
| P4-Based Automated Reasoning (P4-BAR) using Symbolic Execution | Jonathan DiLorenzo | 22m |
Google builds an executable P4 spec, runs P4 Symbolic to generate packets, and diff-tests hardware against a P4-runtime simulator (BMv2/BME2) to check… | ||
| Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet | Nate Foster | 28m |
Lightweight verification leverages Sail RISC V specs compiled to a Rust model and the Connie verifier to check per‑instruction faithful emulation and execution… | ||
| The Software Supporting the JavaScript Language Specification | Michael Ficarra | 31m |
The specification moves from a single Word document to a Git-backed web application spec that scales: ECMarkup generates the HTML, uses Egg/Gram markdown for… | ||
| Trusted JavaScript Language Environments with ESMeta | Jihyeok Park | 27m |
ESMeta extracts a mechanized ECMAScript specification and uses it as an interpreter to automate testing, fuzzing, analysis and partial implementation… | ||
| SpecTec, a Single Source of Truth | Sukyoung Ryu | 26m |
SpecTec defines a single source of truth DSL for WebAssembly semantics that generates LATTE-style formal rules, restructured-markdown prose, an algorithmic… | ||
| Lightweight Semantics Engineering with Redex | Matthew Flatt | 27m |
Redex is presented as a lightweight, Racket-embedded executable semantics DSL for rapid prototyping: write a grammar, reduction rules, judgment forms, then run… | ||
| Programming Languages Must Have Formal Semantics. Period. | Xiaohong Chen | 31m |
Argues that every language gets a machine-checkable formal semantics first and that all tools—interpreter, compiler, verifier, model checker—are automatically… | ||
| nothing matches | ||