A programming language based on CategoryTheory. CharityLanguage isn't TuringComplete, because it lacks general recursion, but it's very expressive. Recursion is based on induction over data-types and is defined formally as the FoldFunction for such data-type.
Innovative organization: based on theory of strong categorical datatypes divided into 2 subclasses: inductive (built up by constructors in the familiar way), and coinductive (broken down by destructors).
All Charity computations terminate (up to user input).
http://www.cpsc.ucalgary.ca/Research/charity/home.html [[BrokenLink]]
CategoryProgrammingLanguage, CategoryBasedLanguage (based on CategoryTheory :-)