Edit detail for Category Theory and FriCAS revision 1 of 1

changed:
-
From BillPage Thu Aug 14 15:54:50 -0700 2008
From: Bill Page
Date: Thu, 14 Aug 2008 15:54:50 -0700
Subject: Some related references
Message-ID: <20080814155450-0700@axiom-wiki.newsynthesis.org>

A Categorical Programming Language

  http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf

by *Tatsuya Hagino*

http://www.tom.sfc.keio.ac.jp/~hagino/index.html.en

**Abstract:** A theory of data types and a programming language based on category theory are presented.

Data types play a crucial role in programming. They enable us to write programs easily and elegantly. Various programming languages have been developed, each of which may use different kinds of data types. Therefore, it becomes important to organize data types systematically so that we can understand the relationship between one data type and another and investigate future directions which lead us to discover exciting new data types.

There have been several approaches to systematically organize data types: algebraic specification methods using algebras, domain theory using complete partially ordered sets and type theory using the connection between logics and data types. Here, we use category theory. Category theory has proved to be remarkably good at revealing the nature of mathematical objects, and we use it to understand the true nature of data types in programming.

We organize data types under a new categorical notion of F,G-dialgebras which is an extension of the notion of adjunctions as well as that of T-algebras. T-algebras are also used in domain theory, but while domain theory needs some primitive data types, like products, to start with, we do not need any. Products, coproducts and exponentiations (i.e. function spaces) are defined exactly like in category theory using adjunctions. F,G-dialgebras also enable us to define the natural number object, the object for finite lists and other familiar data types in programming. Furthermore, their symmetry allows us to have the dual of the natural number object and the object for infinite lists (or lazy lists).

We also introduce a functional programming language in a categorical style. It has no primitive data types nor primitive control structures. Data types are declared using F,G-dialgebras and each data type is associated with its own control structure. For example, natural numbers are associated with primitive recursion. We define the meaning of the language operationally by giving a set of reduction rules. We also prove that any computation in this programming language terminates using Tait's computability method.

A specification language to describe categories is also included. It is used to give a formal semantics to F,G-dialgebras as well as to give a basis to the categorical programming language we introduce.


CHARITY

  http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Charity is a categorical programming language


Computational Category Theory

  http://www.cs.man.ac.uk/~david/categories/

Computational Category Theory is an implementation of concepts and constructions from category theory in the functional programming language Standard ML. The original ideas are due to R.M. Burstall, and it was developed by D. Rydeheard, with help from D.T. Sannella and others in the University of Edinburgh theoretical computer science community.


Prospects for Category Theory in Aldor

  by Saul Youssef, 2004.

http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf

and the following slides:

http://atlas.bu.edu/~youssef/homepage/talks/categories/categories.html


The Microcosm Principle and Concurrency in Coalgebra

  http://www.kurims.kyoto-u.ac.jp/~ichiro/papers/microcosm.pdf

by Ichiro Hasuo, Bart Jacobs and Ana Sokolova

http://www.kurims.kyoto-u.ac.jp/~ichiro/papers.html

Abstract

Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe that the same algebraic theory is interpreted in two different domains in a nested manner, namely: in the category of coalgebras, and in the final coalgebra as an object in it. This phenomenon is what Baez and Dolan have called the microcosm principle, a prototypical example of which is “a monoid in a monoidal category.” In this paper we obtain a formalization of the microcosm principle in which such a nested model is expressed categorically as a suitable lax natural transformation. An application of this account is a general compositionality result which supports modular verification of complex systems.