RPLS

RPLS 2025 with PLDI 2025

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 speci ...