Email: vesely@cpsc.ucalgary.ca Email: vesely@cpsc.ucalgary.ca
The semantics of a programming language can be somewhat peculiar when more emphasis is placed on practical usability than on mathematical elegance in language design. An alternative approach has been to base a programming language on some predetermined mathematical formalization. charity is an example of such a language.
One of the goals of our work is to capture both the syntax and semantics of charity as cleanly as possible in the form of a type theory. Of course the translation of charity term logic to combinators is suggestive of the connection to the categorical semantics. What we are interested in is a somewhat more explicit connection between the term logic and the category theory.
The intention is to gain an understanding of how the categorical setting evolves as the programmer provides a sequence of charity declarations, and ultimately builds a charity program. We are developing a type theory with the hope of capturing both of these veins in a constructive and elegant fashion.
Dr. Robin Cockett, Tom Fukushima, Dave Spooner, Barry Yee, Ulrich Hensel, Marc Schroeder, and Charles Tuckey.
Return to Charity home page.