ABOUT CHARITY
dc.contributor.author | Fukushima, Tom | eng |
dc.contributor.author | Cockett, Robin | eng |
dc.date.accessioned | 2008-02-26T20:30:15Z | |
dc.date.available | 2008-02-26T20:30:15Z | |
dc.date.computerscience | 1999-05-27 | eng |
dc.date.issued | 1992-06-01 | eng |
dc.description.abstract | Charity is a categorical programming language based on distributive categories (in the sense of Schanuel and Lawvere) with strong datatypes (in the sense of Hagino). Distributive categories come with a term logic which can express most standard programs; and they are fundamental to computer science because they permit proof by case analysis and, when strong datatypes are introduced, proof by structural induction. Charity is functional and polymorphic in style, and is strongly normalizing. As a categorical programming language it provides a unique marriage of computer science and mathematical thought. The above aspects are particularly important for the production of verified programs as the naturality of morphisms gives us ``theorems for free'', termination proofs are not required, and mathemathical specifications can be used. | eng |
dc.description.notes | We are currently acquiring citations for the work deposited into this collection. We recognize the distribution rights of this item may have been assigned to another entity, other than the author(s) of the work.If you can provide the citation for this work or you think you own the distribution rights to this work please contact the Institutional Repository Administrator at digitize@ucalgary.ca | eng |
dc.identifier.department | 1992-480-18 | eng |
dc.identifier.doi | http://dx.doi.org/10.11575/PRISM/30563 | |
dc.identifier.uri | http://hdl.handle.net/1880/45460 | |
dc.language.iso | Eng | eng |
dc.publisher.corporate | University of Calgary | eng |
dc.publisher.faculty | Science | eng |
dc.subject | Computer Science | eng |
dc.title | ABOUT CHARITY | eng |
dc.type | unknown | |
thesis.degree.discipline | Computer Science | eng |