Abstract
Attribute Grammars (AGs) are a domain-specific language for functional and composable descriptions of tree traversals. Given such a description, it is not immediately clear how to state and prove properties of AGs formally. To meet this challenge, we apply dependent types to AGs. In a dependently typed AG, the type of an attribute may refer to values of attributes. The type of an attribute is an invariant, the value of an attribute a proof for that invariant. Additionally, when an AG is cycle-free, the composition of the attributes is logically consistent. We present a lightweight approach using a preprocessor in combination with the dependently typed language Agda.
Original language | English |
---|---|
Title of host publication | IFL 2010 |
Publisher | Springer |
Pages | 105–120 |
ISBN (Electronic) | 978-3-642-24276-2 |
ISBN (Print) | 978-3-642-24275-5 |
DOIs | |
Publication status | Published - 2011 |