On 12/11/14, Dee Roytenberg <roytenberg.d@gmail.com> wrote:
Many thanks to everyone who replied, with enough suggestions to fill a bookshelf!
Just to add one remark: while there is a lot of literature this relation, at the heart of it there is one single simple but profound dictionary which translates category theory <-> type theory <-> computation such that these three subjects become, essentially, just three different faces of one single phenomenon. Since this is so neat, Bob Harper once referred to this as "computational trinitarianism". A hyperlinked version of the dictionary, with further pointers, is here: http://ncatlab.org:8080/nlab/show/computational+trinitarianism Best, Urs [For admin and other information see: http://www.mta.ca/~cat-dist/ ]