  Rascal is a high-level transformation language that aims to simplify software
language engineering tasks like defining program syntax, analyzing and
transforming programs, and performing code generation. The language provides
several features including built-in collections (lists, sets, maps), algebraic
data-types, powerful pattern matching operations with backtracking, and
high-level traversals supporting multiple strategies. Interaction between
different language features can be difficult to comprehend, since most features
are semantically rich. The report provides a well-defined formal semantics for
a large subset of Rascal, called Rascal Light, suitable for developing formal
techniques, e.g., type systems and static analyses. Additionally, the report
states and proofs a series of interesting properties of the semantics,
including purity of backtracking, strong typing, partial progress and the
existence of a terminating subset.
