On 17 September at 14:00, Prof. J. Robin B. Cockett will be promoted to Doctor honoris causa of TalTech at the University's anniversary ceremony for his outstanding and long-term dedicated contribution and goodwill in enhancing the competence and international visibility of Tallinn University of Technology in the field of mathematics and computer science.

In this connection, Robin is visiting Department of Software Science's High-assurance Software Laboratory to give a public lecture on 16 September at 15:00. The topic is Robin's relationship to programming languages - their design and implementation: "Programming languages I have known and loved". See the abstract below.

The talk will take place in CYB-101 and also can be followed via Zoom, the details are below.

Programming languages I have known and loved

Robin Cockett
University of Calgary, Canada

Abstract: It all started with Tatsuya Hagino's PhD thesis (1986) in which he showed how category theory could be used directly as a programming language. Computation in Tatsuya's system was delivered by rewriting categorical combinators -- similarly to Curien's categorical abstract machine (CAM). The downside was that you had to write programs in categorical combinators which was downright impossible ...

Dwight Spencer and I showed how one could translate from a more useable term logic into the categorical combinators. This became the programming language Charity. The computational power of Charity was delivered by the inductive and coinductive data declarations. Furthermore, in order to enhance the expressive power we allowed definitions of "combinators".

The resulting setting was not Cartesian closed: so, one had to program in a purely first-order manner. This, it turned out, was a bit of a problem because one could not write efficient programs! To overcome this defect we increased the power of coinductive definitions to allow "higher-order coinductive" data. In this way the computational power of Charity was still delivered by data declarations but one could declare the exponential type as a coinductive data type if you wanted to write higher-order programs.

Charity development stopped in about 1996. It was a sequential programming language and the world had meanwhile become very concurrent! Thus, I was determined to produce a categorical concurrent language. This led to the development of CaMPL which stands for "Categorical Message Passing Language". In CaMPL one can write write concurrent programs (and parallel programs) with typed communication channels. For example, one can write airline booking systems.

Notably, in (a strongly typed version of) CaMPL one cannot write programs which have deadlocks or livelocks ... however, the language seems to be quite expressive. I shall introduce you to the ideas of CAMPL which are strongly influenced by Charity ... and what I had learned from its development.

Topic: Robin Cockett Honorary Doctor lecture
Time: Sep 16, 2024 15:00 Helsinki

Join Zoom Meeting
https://zoom.us/j/99766170671?pwd=M3uulFSafrv5faqznWKvxowh8l19LJ.1

Meeting ID: 997 6617 0671
Passcode: 631059

Everyone interested is most welcome!