Aiding Dependent Type Checking with Rewrite Rules Export

@misc{citeulike:392501, abstract = {Dependent type checking in Cayenne often fails when the programmer has relied on non-trivial properties of functions that are used in types. For instance, associativity of addition on natural numbers does not follow immediately from the function definition, but it may be required during the type checking process. We propose to tackle this problem by allowing the programmer to annotate programs with rewrite rules whenever such additional properties are required. We discuss two motivating...}, author = {Huencke, Yorck and de Moor, Oege}, citeulike-article-id = {392501}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5035}, keywords = {dependent-types, rewriting}, posted-at = {2005-11-14 20:07:17}, priority = {5}, title = {Aiding Dependent Type Checking with Rewrite Rules}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5035} }

TY - GEN ID - citeulike:392501 L3 - citeulike-article-id:392501 N2 - Dependent type checking in Cayenne often fails when the programmer has relied on non-trivial properties of functions that are used in types. For instance, associativity of addition on natural numbers does not follow immediately from the function definition, but it may be required during the type checking process. We propose to tackle this problem by allowing the programmer to annotate programs with rewrite rules whenever such additional properties are required. We discuss two motivating... TI - Aiding Dependent Type Checking with Rewrite Rules KW - dependent-types KW - rewriting AU - Huencke, Yorck AU - de Moor, Oege UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.5035 ER -