Sciweavers

MST
2008

Datatype-Generic Termination Proofs

13 years 3 months ago
Datatype-Generic Termination Proofs
Abstract. Datatype-generic programs are programs that are parameterised by a datatype. We review the allegorical foundations of a methodology of designing datatype-generic programs. The notion of F-reductivity, where F parametrises a datatype, is reviewed and a number of its properties are presented. The properties are used to give concise, effective proofs of termination of a number of datatype-generic programming schemas. The paper concludes with a concise proof of the well-foundedness of a datatype-generic occurs-in relation.
Roland Carl Backhouse, Henk Doornbos
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where MST
Authors Roland Carl Backhouse, Henk Doornbos
Comments (0)