Datatype-generic termination proofs
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 prop...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Springer
2008
|
| Online Access: | https://eprints.nottingham.ac.uk/1858/ |
| _version_ | 1848790675755106304 |
|---|---|
| author | Backhouse, Roland Doornbos, Henk |
| author_facet | Backhouse, Roland Doornbos, Henk |
| author_sort | Backhouse, Roland |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-14T18:16:23Z |
| format | Article |
| id | nottingham-1858 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:16:23Z |
| publishDate | 2008 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-18582020-05-04T20:27:09Z https://eprints.nottingham.ac.uk/1858/ Datatype-generic termination proofs Backhouse, Roland Doornbos, Henk 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. Springer 2008-12 Article PeerReviewed Backhouse, Roland and Doornbos, Henk (2008) Datatype-generic termination proofs. Theory of Computing Systems, 43 (3-4). pp. 362-393. ISSN 1433-0490 http://link.springer.com/article/10.1007%2Fs00224-007-9056-z doi:10.1007/s00224-007-9056-z doi:10.1007/s00224-007-9056-z |
| spellingShingle | Backhouse, Roland Doornbos, Henk Datatype-generic termination proofs |
| title | Datatype-generic termination proofs |
| title_full | Datatype-generic termination proofs |
| title_fullStr | Datatype-generic termination proofs |
| title_full_unstemmed | Datatype-generic termination proofs |
| title_short | Datatype-generic termination proofs |
| title_sort | datatype-generic termination proofs |
| url | https://eprints.nottingham.ac.uk/1858/ https://eprints.nottingham.ac.uk/1858/ https://eprints.nottingham.ac.uk/1858/ |