Researchers have presented numerous frameworks for mechanizing the definition of programming languages. Ott takes a language definition in ASCII notation as input and generates various versions of the definition, including LaTeX, Coq, and Isabelle/HOL. K generates tools such as interpreters, model checkers, and verifiers, from language definitions encoded in K’s term rewriting system. PLT Redex supports the specification and debugging of language semantics using randomized test generation. Skeletal Semantics describes and manipulates language semantics and can generate OCaml interpreters and Coq formalizations. Some frameworks are more specialized. Sail supports processor instruction set architecture definitions, generates SMT encodings, theorem prover definitions, and LaTeX document fragments. ESMeta generates mechanized JavaScript semantics and various tools from prose specifications of JavaScript. SpecTec generates a typeset specification, including formal definitions and prose descriptions, and a meta-level interpreter from a SpecTec definition of the WebAssembly semantics.
Some of these tools have been applied to mechanize the definition of real-world programming languages and have been adopted by language standardization organizations to verify or generate normative language specifications. Sail supports the complete ISA specifications for several Arm architectures, automatically translated from the Arm-internal ASL reference (as used in the Arm reference manual). ESMeta is integrated into the CI systems of ECMA-262, the JavaScript language specification, and Test262, the JavaScript test suite. The WebAssembly Community Group has agreed to adopt SpecTec as a toolchain for WebAssembly specifications (when it is ready). Inspired by these achievements, researchers are applying similar techniques to other languages such as P4 and Rust. In this workshop, we will discuss different approaches to mechanizing the definition and implementation of real-world programming languages.
Call for Participants
This workshop will be centered around a small number of invited talks on the development, use, and maintenance of real-world programming language specifications, interspersed with panel discussions and broader discussion among the attendees.
