@article {DBLP:journals/entcs/AlmeidaPV07,
	title = {A Local Graph-rewriting System for Deciding Equality in Sum-product Theories},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {176},
	number = {1},
	year = {2007},
	pages = {139-163},
	abstract = {<p>In this paper we give a graph-based decision procedure for a calculus with sum and product types. Although our motivation comes from the Bird-Meertens approach to reasoning algebraically about functional programs, the language used here can be seen as the internal language of a category with binary products and coproducts. As such, the decision procedure presented has independent interest.<br />
A standard approach based on term rewriting would work modulo a set of equations; the present work proposes a simpler approach, based on graph-rewriting. We show in turn how the system covers reflection equational laws, fusion laws, and cancellation laws.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jba/files/06sum-product.pdf},
	author = {Jos{\'e} Bacelar Almeida and Jorge Sousa Pinto and Miguel Vila{\c c}a}
}