5 added 40 characters in body

Since sdvccv already pointed out a number of good sources for learning category theory as applied to CS, I will try and provide some guide posts.

My favorite book on the subject is Practical Foundations of Mathematics by Paul Taylor since he does a really good job of giving you a big picture (unfortunately he doesn't always give you enough details if you don't already have a logic background). Bart Jacobs book Categorical Logic and Type Theory is also very readable.

In general I think the most important thing to understand in order to apply categories to computer science is the Curry-Howard-Lambek correspondence which loosely states that lambda calculii, intuitionist logics, and cartesian closed categories (categories where you have products and function spaces) are the same thing. Proofs and Types which was transcribed from some of Girard's lecture notes is an excellent source for the Curry-Howard part of the correspondence. Steve Awodey's book and these notes by Samson Abramsky are good places to see this translated into categorical language. For connections to Topoi Mac Lane's Sheaves in Geometry and Logic looks good.

Next you will probably want to learn about categorical and universal algebra. One of the more immediate and accessible applications of these ideas is the theory of algebraic data types (categorically: initial algebras for polynomial functors) and maps and folds between them. Monads are also a part of this subject since they are type constructors (endofunctors) that also have a multiplication and unit. Haskell do notation corresponds to forming the Kliesli category for a monad.

The nascent field of universal coalgebra has been very useful for formalizing notions of state and observation. Bart Jacobs recently did some work on coalgebraic semantics for classes in object oriented languages. There are also some emerging connections between coalgebra and modal logic.

Finally, if you aren't worn out you may want to learn about Stone duality which is a way of relating "logics of observable properties" and topology. For computer scientist Stone duality is primarily useful for giving a logical interpretation to domain theory, but mathematicians may recognize the duality between commutative rings and Zariski spectra as a special case.

4 added 186 characters in body

Since sdvccv already pointed out a number of good sources for learning category theory as applied to CS, I will try and provide some guide posts.

My favorite book on the subject is Practical Foundations of Mathematics by Paul Taylor since he does a really good job of giving you a big picture (unfortunately he doesn't always give you enough details if you don't already have a logic background).

In general I think the most important thing to understand in order to apply categories to computer science is the Curry-Howard-Lambek correspondence which loosely states that lambda calculii, intuitionist logics, and cartesian closed categories (categories where you have products and function spaces) are the same thing. Proofs and Types which was transcribed from some of Girard's lecture notes is an excellent source for the Curry-Howard part of the correspondence. Steve Awodey's book and these notes by Samson Abramsky are good places to see this translated into categorical language.

Next you will probably want to learn about categorical and universal algebra. One of the more immediate and accessible applications of these ideas is the theory of algebraic data types (categorically: initial algebras for polynomial functors) and maps and folds between them. Monads are also a part of this subject since they are type constructors (endofunctors) that also have a multiplication and unit. Haskell do notation corresponds to forming the Kliesli category for a monad.

The nascent field of universal coalgebra has been very useful for formalizing notions of state and observation. Bart Jacobs recently did some work on coalgebraic semantics for classes in object oriented languages. There are also some emerging connections between coalgebra and modal logic.

Finally, if you aren't worn out you may want to learn about Stone duality which is a way of relating "logics of observable properties" and topology. For computer scientist Stone duality is primarily useful for giving a logical interpretation to domain theory, but mathematicians may recognize the duality between commutative rings and Zariski spectra as a special case.

Since sdvccv already pointed out a number of good sources for learning category theory as applied to CS, I will try and provide some guide posts.

My favorite book on the subject is Practical Foundations of Mathematics by Paul Taylor since he does a really good job of giving you a big picture (unfortunately he doesn't always give you enough details if you don't already have a logic background).

In general I think the most important thing to understand in order to apply categories to computer science is the Curry-Howard-Lambek correspondence which loosely states that lambda calculii, intuitionist logics, and cartesian closed categories (categories where you have products and function spaces) are the same thing. Proofs and Types(www.cs.manchester.ac.uk/~pt/stable/prot.pdf) which was transcribed from some of Girard's lecture notes is an excellent source for the Curry-Howard part of the correspondence. Steve Awodey's book and these (web.comlab.ox.ac.uk/people/Bob.Coecke/AbrNikos.pdf) notes by Samson Abramsky are a good place places to see this translated into categorical language.

Next you will probably want to learn about categorical and universal algebra. One of the more immediate and accessible applications of these ideas is the theory of algebraic data types (categorically: initial algebras for polynomial functors) and maps and folds between them(www.cs.ut.ee/~varmo/papers/thesis.pdf). . Monads are also a part of this subject since they are type constructors (endofunctors) that also have a multiplication and unit. Haskell do notation corresponds to forming the Kliesli category for a monad(lambda-the-ultimate.org/node/1183)..

The nascent field of universal coalgebra has been very useful for formalizing notions of state and observation(www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf). . Bart Jacobs recently did some work on coalgebraic semantics for (citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.7619) classes in object oriented languages. There are also some emerging connections between coalgebra and modal logic.

Finally if aren't worn out you may want to learn about Stone duality (www.amazon.com/Topology-Cambridge-Theoretical-Computer-Science/dp/0521576512) which is a way of relating "logics of observable properties" and topology. For computer scientist this Stone duality is primarily interesting because of useful giving a logical interpretation to domain theory, but mathematicians may recognize the duality between commutative rings and Zariski spectra as a special case.

PS - Sorry these weren't hyperlinks. Until I get some reputation I can't post more than one.

2 added 10 characters in body
1