From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5125 Path: news.gmane.org!not-for-mail From: Bas Spitters Newsgroups: gmane.science.mathematics.categories Subject: Re: categories and formal verification Date: Tue, 8 Sep 2009 15:53:17 +0200 Message-ID: Reply-To: Bas Spitters NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1252457212 18122 80.91.229.12 (9 Sep 2009 00:46:52 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 9 Sep 2009 00:46:52 +0000 (UTC) To: David CHEMOUIL , Original-X-From: categories@mta.ca Wed Sep 09 02:46:45 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 1MlBKe-0004Lf-4o for gsmc-categories@m.gmane.org; Wed, 09 Sep 2009 02:46:44 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MlAcE-0001iG-6D for categories-list@mta.ca; Tue, 08 Sep 2009 21:00:50 -0300 Content-Disposition: inline Original-Content-Transfer-Encoding: quoted-printable Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5125 Archived-At: We used monads and applicative functors to verify an implementation real=20 integration. We found CT to be convenient in the process: A computer verified, monadic, functional implementation of the integral. Russell O'Connor, Bas Spitters http://arxiv.org/abs/0809.1552 Abstract: We provide a computer verified exact monadic functional=20 implementation of the Riemann integral in type theory. Together with previo= us=20 work by O=E2=80=99Connor, this may be seen as the beginning of the realizat= ion of=20 Bishop=E2=80=99s vision to use constructive mathematics as a programming la= nguage for=20 exact analysis. Best regards, Bas On Tuesday 08 September 2009 09:20:52 David CHEMOUIL wrote: > 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 th= is > 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 th= is > topic. > > Regards, > > dc [For admin and other information see: http://www.mta.ca/~cat-dist/ ]