ABOUT CHARITY
Date
1992-06-01
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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.
Description
Keywords
Computer Science