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. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Middelkoop, A., Dijkstra, A., & Swierstra, S. D. (2011). Dependently typed attribute grammars. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6647 LNCS, pp. 105–120). https://doi.org/10.1007/978-3-642-24276-2_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
