Computational Category Theory
by D.E. Rydeheard, R.M. Burstall
Number of pages: 263
This book is an account of a project in which basic constructions of category theory are expressed as computer programs. The programs are written in a functional programming language, called ML, and have been executed on examples. The authors have used these programs to develop algorithms for the unification of terms and to implement a categorical semantics. In general, this book is a bridge-building exercise between category theory and computer programming. These efforts are a first attempt at connecting the abstract mathematics with concrete programs, whereas others have applied categorical ideas to the theory of computation.
Home page url
Download or read it online for free here:
by Peter Selinger - Dalhousie University
Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, type inference, etc.
by Kenneth Slonneger, Barry L. Kurtz - Addison Wesley Longman
The book presents the typically difficult subject of formal methods in an informal, easy-to-follow manner. Readers with a basic grounding in discreet mathematics will be able to understand the practical applications of these difficult concepts.
by Robert Harper
Provides an account of the role of type theory in programming language design and implementation. The stress is on the use of types as a tool for analyzing programming language features and studying their implementation.
by Andrea Asperti, Giuseppe Longo - MIT Press
Here is an introduction to category theory for the working computer scientist. It is a self-contained introduction to general category theory and the mathematical structures that constitute the theoretical background.