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.

• Type: Journal
• Year: 2008
• Where: MST
• Authors: Roland Carl Backhouse, Henk Doornbos
• Keywords: Allegorical Foundations, Datatype-generic Programming Schemas, Datatype-generic Programs, MST 2008