Dependently Typed Attribute Grammars

A. Middelkoop; A. Dijkstra; S.D. Swierstra

doi:10.1007/978-3-642-24276-2_7

Dependently Typed Attribute Grammars

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 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	https://doi.org/10.1007/978-3-642-24276-2_7
Publication status	Published - 2011

Bibliographical note

IFL

Access to Document

10.1007/978-3-642-24276-2_7

Depend
Open Access (free)
Submitted manuscript, 126 KB

Cite this

@inproceedings{80049edc09c549f4bea6c2f3c3c83e95,

title = "Dependently Typed Attribute Grammars",

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. ",

author = "A. Middelkoop and A. Dijkstra and S.D. Swierstra",

note = "IFL",

year = "2011",

doi = "10.1007/978-3-642-24276-2\_7",

language = "English",

isbn = "978-3-642-24275-5",

pages = "105–120",

booktitle = "IFL 2010",

publisher = "Springer",

}

TY - GEN

T1 - Dependently Typed Attribute Grammars

AU - Middelkoop, A.

AU - Dijkstra, A.

AU - Swierstra, S.D.

N1 - IFL

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-24276-2_7

DO - 10.1007/978-3-642-24276-2_7

M3 - Conference contribution

SN - 978-3-642-24275-5

SP - 105

EP - 120

BT - IFL 2010

PB - Springer

ER -

Dependently Typed Attribute Grammars

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this