The Formal Semantics of Rascal Light

TL;DR

This paper presents a formal semantics for Rascal Light, a subset of the Rascal language, enabling rigorous analysis and verification of program transformations and language features.

Contribution

It provides a formal, well-defined semantics for Rascal Light, facilitating the development of formal techniques like type systems and static analyses.

Findings

Proves purity of backtracking in Rascal Light

Establishes strong typing and partial progress properties

Identifies a terminating subset of Rascal Light

Abstract

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.