Skip to main content

Research Repository

Advanced Search

Datatype-generic termination proofs

Backhouse, Roland; Doornbos, Henk


Roland Backhouse

Henk Doornbos


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.


Backhouse, R., & Doornbos, H. (2008). Datatype-generic termination proofs. Theory of Computing Systems, 43(3-4),

Journal Article Type Article
Publication Date Dec 1, 2008
Deposit Date Jan 7, 2013
Publicly Available Date Jan 7, 2013
Journal Theory of Computing Systems
Print ISSN 1432-4350
Electronic ISSN 1433-0490
Publisher Springer Verlag
Peer Reviewed Peer Reviewed
Volume 43
Issue 3-4
Public URL
Publisher URL
Additional Information The original publication is available at


Downloadable Citations