P5 — A Rewriting Logic Approach to the Design and Analysis of Object-Oriented Languages

Abstract

Rewriting logic semantics provides an environment for defining new and existing languages. These language definitions are formal and executable, providing a language interpreter for defined languages almost for free while also providing a framework for building language analysis tools, such as type checkers, abstract interpreters, and model checkers. Multiple existing object-oriented languages, including Java and Beta, have been defined, while a new research language, KOOL, has been created as a platform for experimenting with language features and type systems. The openness of the framework allows the use of various front-end parsers and back-end execution engines.