From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5124 Path: news.gmane.org!not-for-mail From: David CHEMOUIL Newsgroups: gmane.science.mathematics.categories Subject: categories and formal verification Date: Tue, 8 Sep 2009 09:20:52 +0200 Message-ID: Reply-To: David CHEMOUIL NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1252418151 16746 80.91.229.12 (8 Sep 2009 13:55:51 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 8 Sep 2009 13:55:51 +0000 (UTC) To: categories Original-X-From: categories@mta.ca Tue Sep 08 15:55:44 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1Ml1Aa-0007Fj-Pb for gsmc-categories@m.gmane.org; Tue, 08 Sep 2009 15:55:40 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Ml0ZS-0005i4-Gh for categories-list@mta.ca; Tue, 08 Sep 2009 10:17:18 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5124 Archived-At: Dear colleagues, Some colleagues of mine and myself are currently investigating categorical approaches to component-based development for software, in the spirit of J. L. Fiadeiro's work or of the coalgebra community. Being new to the discipline, it also implies for them quite some work in basic CT itself. Hence, they're looking for some kind of reason making this tedious process worth enduring. Elegance of CT is one such reason, Goguen's or Ehrig's arguments in a few articles are others. But, although my colleagues, are pretty convinced by the "constructive" aspects of CT applied to such matters, they don't see how CT can provide support in *verifying* things about systems under study (e.g what does CT approaches bring to check the absence of deadlocks in a concurrent system?). I couldn't find convincing examples, even in Goguen's Manifesto, so I wondered whether you had good arguments and/or references to such convincing work, that would give them the impetus to continue studying this topic. Regards, dc -- David CHEMOUIL ONERA/DTIM http://www.onera.fr/staff/david-chemouil [For admin and other information see: http://www.mta.ca/~cat-dist/ ]