Datatype-generic termination proofs
| Autor: | Henk Doornbos, Roland Backhouse |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2008 |
| Předmět: |
Generic programming
Relation (database) Programming language Computer science Software_PROGRAMMINGTECHNIQUES Relation algebra Mathematical proof computer.software_genre Theoretical Computer Science Software development process TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Symbol (programming) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Theory of computation Software_PROGRAMMINGLANGUAGES computer |
| ISSN: | 1432-4350 1433-0490 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink