Dependently Typed Attribute Grammars

A. Middelkoop, A. Dijkstra, S.D. Swierstra

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    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 languageEnglish
    Title of host publicationIFL 2010
    PublisherSpringer
    Pages105–120
    ISBN (Electronic)978-3-642-24276-2
    ISBN (Print)978-3-642-24275-5
    DOIs
    Publication statusPublished - 2011

    Bibliographical note

    IFL

    Fingerprint

    Dive into the research topics of 'Dependently Typed Attribute Grammars'. Together they form a unique fingerprint.

    Cite this