Parsing K definitions

This paper describes our approach in parsing a \K\ definition. The difficulty of the problem is given by the nature of the \K-framework, where the user can define the operational semantics of a language by inserting pieces of concrete syntax in the \K\ code in a natural way. Our main contribution shows how to make use of SDF and the disambiguation mechanisms in the context of \K-framework.

Sidebar