Datatype-generic termination proofs

Backhouse, Roland; Doornbos, Henk

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.

Citation

Backhouse, R., & Doornbos, H. (2008). Datatype-generic termination proofs. Theory of Computing Systems, 43(3-4), https://doi.org/10.1007/s00224-007-9056-z

• 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
• DOI: https://doi.org/10.1007/s00224-007-9056-z
• Public URL: https://nottingham-repository.worktribe.com/output/1015043
• Publisher URL: http://link.springer.com/article/10.1007%2Fs00224-007-9056-z
• Additional Information: The original publication is available at www.springerlink.com